DEFINITION sn3_gen_cflat()
TYPE =
       ∀f:F.∀c:C.∀u:T.∀t:T.(sn3 (CHead c (Flat f) u) t)→(sn3 c t)
BODY =
        assume f: F
        assume c: C
        assume u: T
        assume t: T
        suppose H: sn3 (CHead c (Flat f) u) t
          we proceed by induction on H to prove sn3 c t
             case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 (CHead c (Flat f) u) t1 t2)→(sn3 (CHead c (Flat f) u) t2) ⇒
                the thesis becomes sn3 c t1
                (H1) by induction hypothesis we know ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 (CHead c (Flat f) u) t1 t2)→(sn3 c t2)
                    assume t2: T
                    suppose H2: (eq T t1 t2)→∀P:Prop.P
                    suppose H3: pr3 c t1 t2
                      by (pr3_cflat . . . H3 . .)
                      we proved pr3 (CHead c (Flat f) u) t1 t2
                      by (H1 . H2 previous)
                      we proved sn3 c t2
                   we proved ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2)
                   by (sn3_sing . . previous)
sn3 c t1
          we proved sn3 c t
       we proved ∀f:F.∀c:C.∀u:T.∀t:T.(sn3 (CHead c (Flat f) u) t)→(sn3 c t)