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