DEFINITION clt_thead()
TYPE =
∀k:K.∀u:T.∀c:C.(clt c (CTail k u c))
BODY =
assume k: K
assume u: T
assume c: C
we proceed by induction on c to prove clt c (CTail k u c)
case CSort : n:nat ⇒
the thesis becomes clt (CSort n) (CTail k u (CSort n))
by (clt_head . . .)
we proved clt (CSort n) (CHead (CSort n) k u)
clt (CSort n) (CTail k u (CSort n))
case CHead : c0:C k0:K t:T ⇒
the thesis becomes clt (CHead c0 k0 t) (CTail k u (CHead c0 k0 t))
(H) by induction hypothesis we know clt c0 (CTail k u c0)
by (clt_cong . . H . .)
we proved clt (CHead c0 k0 t) (CHead (CTail k u c0) k0 t)
clt (CHead c0 k0 t) (CTail k u (CHead c0 k0 t))
we proved clt c (CTail k u c)
we proved ∀k:K.∀u:T.∀c:C.(clt c (CTail k u c))