DEFINITION pr3_flat()
TYPE =
       ∀c:C
         .∀u1:T
           .∀u2:T
             .pr3 c u1 u2
               →∀t1:T.∀t2:T.(pr3 c t1 t2)→∀f:F.(pr3 c (THead (Flat f) u1 t1) (THead (Flat f) u2 t2))
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr3 c u1 u2
        assume t1: T
        assume t2: T
        suppose H0: pr3 c t1 t2
        assume f: F
          by (pr3_cflat . . . H0 . .)
          we proved pr3 (CHead c (Flat f) u2) t1 t2
          by (pr3_head_12 . . . H . . . previous)
          we proved pr3 c (THead (Flat f) u1 t1) (THead (Flat f) u2 t2)
       we proved 
          ∀c:C
            .∀u1:T
              .∀u2:T
                .pr3 c u1 u2
                  →∀t1:T.∀t2:T.(pr3 c t1 t2)→∀f:F.(pr3 c (THead (Flat f) u1 t1) (THead (Flat f) u2 t2))