DEFINITION pr3_cflat()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t1 t2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c t1 t2
          we proceed by induction on H to prove ∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t1 t2)
             case pr3_refl : t:T ⇒
                the thesis becomes ∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t t)
                    assume f: F
                    assume v: T
                      by (pr3_refl . .)
                      we proved pr3 (CHead c (Flat f) v) t t
∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t t)
             case pr3_sing : t3:T t4:T H0:pr2 c t4 t3 t5:T :pr3 c t3 t5 ⇒
                the thesis becomes ∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t4 t5)
                (H2) by induction hypothesis we know ∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t3 t5)
                    assume f: F
                    assume v: T
                      (h1) 
                         by (pr2_cflat . . . H0 . .)
pr2 (CHead c (Flat f) v) t4 t3
                      end of h1
                      (h2) 
                         by (H2 . .)
pr3 (CHead c (Flat f) v) t3 t5
                      end of h2
                      by (pr3_sing . . . h1 . h2)
                      we proved pr3 (CHead c (Flat f) v) t4 t5
∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t4 t5)
          we proved ∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t1 t2)
       we proved ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→∀f:F.∀v:T.(pr3 (CHead c (Flat f) v) t1 t2)