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 =
Show proof