DEFINITION pc3_thin_dx()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pc3 c t1 t2)→∀u:T.∀f:F.(pc3 c (THead (Flat f) u t1) (THead (Flat f) u t2))
BODY =
Show proof