DEFINITION chead_ctail()
TYPE =
       ∀c:C.∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c k t) (CTail h u d))
BODY =
       assume c: C
          we proceed by induction on c to prove ∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c k t) (CTail h u d))
             case CSort : n:nat ⇒
                the thesis becomes ∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CSort n) k t) (CTail h u d))
                    assume t: T
                    assume k: K
                      by (refl_equal . .)
                      we proved eq C (CHead (CSort n) k t) (CHead (CSort n) k t)
                      that is equivalent to eq C (CHead (CSort n) k t) (CTail k t (CSort n))
                      by (ex_3_intro . . . . . . . previous)
                      we proved ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CSort n) k t) (CTail h u d)
∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CSort n) k t) (CTail h u d))
             case CHead : c0:C k:K t:T ⇒
                the thesis becomes ∀t0:T.∀k0:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d))
                (H) by induction hypothesis we know ∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c0 k t) (CTail h u d))
                    assume t0: T
                    assume k0: K
                      (H_x) 
                         by (H . .)
ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c0 k t) (CTail h u d)
                      end of H_x
                      (H0) consider H_x
                      we proceed by induction on H0 to prove ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d)
                         case ex_3_intro : x0:K x1:C x2:T H1:eq C (CHead c0 k t) (CTail x0 x2 x1) ⇒
                            the thesis becomes ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d)
                               by (refl_equal . .)
                               we proved eq C (CHead (CTail x0 x2 x1) k0 t0) (CHead (CTail x0 x2 x1) k0 t0)
                               that is equivalent to eq C (CHead (CTail x0 x2 x1) k0 t0) (CTail x0 x2 (CHead x1 k0 t0))
                               by (ex_3_intro . . . . . . . previous)
                               we proved ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CTail x0 x2 x1) k0 t0) (CTail h u d)
                               by (eq_ind_r . . . previous . H1)
ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d)
                      we proved ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d)
∀t0:T.∀k0:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d))
          we proved ∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c k t) (CTail h u d))
       we proved ∀c:C.∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c k t) (CTail h u d))