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