DEFINITION sn3_gen_head()
TYPE =
       ∀k:K.∀c:C.∀u:T.∀t:T.(sn3 c (THead k u t))→(sn3 c u)
BODY =
       assume k: K
          we proceed by induction on k to prove ∀c:C.∀u:T.∀t:T.(sn3 c (THead k u t))→(sn3 c u)
             case Bind : b:B ⇒
                the thesis becomes ∀c:C.∀u:T.∀t:T.∀H:(sn3 c (THead (Bind b) u t)).(sn3 c u)
                    assume c: C
                    assume u: T
                    assume t: T
                    suppose H: sn3 c (THead (Bind b) u t)
                      (H_x) 
                         by (sn3_gen_bind . . . . H)
land (sn3 c u) (sn3 (CHead c (Bind b) u) t)
                      end of H_x
                      (H0) consider H_x
                      we proceed by induction on H0 to prove sn3 c u
                         case conj : H1:sn3 c u :sn3 (CHead c (Bind b) u) t ⇒
                            the thesis becomes the hypothesis H1
                      we proved sn3 c u
∀c:C.∀u:T.∀t:T.∀H:(sn3 c (THead (Bind b) u t)).(sn3 c u)
             case Flat : f:F ⇒
                the thesis becomes ∀c:C.∀u:T.∀t:T.∀H:(sn3 c (THead (Flat f) u t)).(sn3 c u)
                    assume c: C
                    assume u: T
                    assume t: T
                    suppose H: sn3 c (THead (Flat f) u t)
                      (H_x) 
                         by (sn3_gen_flat . . . . H)
land (sn3 c u) (sn3 c t)
                      end of H_x
                      (H0) consider H_x
                      we proceed by induction on H0 to prove sn3 c u
                         case conj : H1:sn3 c u :sn3 c t ⇒
                            the thesis becomes the hypothesis H1
                      we proved sn3 c u
∀c:C.∀u:T.∀t:T.∀H:(sn3 c (THead (Flat f) u t)).(sn3 c u)
          we proved ∀c:C.∀u:T.∀t:T.(sn3 c (THead k u t))→(sn3 c u)
       we proved ∀k:K.∀c:C.∀u:T.∀t:T.(sn3 c (THead k u t))→(sn3 c u)