DEFINITION pr3_thin_dx()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→∀u:T.∀f:F.(pr3 c (THead (Flat f) u t1) (THead (Flat f) u t2))
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c t1 t2
        assume u: T
        assume f: F
          we proceed by induction on H to prove pr3 c (THead (Flat f) u t1) (THead (Flat f) u t2)
             case pr3_refl : t:T ⇒
                the thesis becomes pr3 c (THead (Flat f) u t) (THead (Flat f) u t)
                   by (pr3_refl . .)
pr3 c (THead (Flat f) u t) (THead (Flat f) u t)
             case pr3_sing : t0:T t3:T H0:pr2 c t3 t0 t4:T :pr3 c t0 t4 ⇒
                the thesis becomes pr3 c (THead (Flat f) u t3) (THead (Flat f) u t4)
                (H2) by induction hypothesis we know pr3 c (THead (Flat f) u t0) (THead (Flat f) u t4)
                   by (pr2_thin_dx . . . H0 . .)
                   we proved pr2 c (THead (Flat f) u t3) (THead (Flat f) u t0)
                   by (pr3_sing . . . previous . H2)
pr3 c (THead (Flat f) u t3) (THead (Flat f) u t4)
          we proved pr3 c (THead (Flat f) u t1) (THead (Flat f) u t2)
       we proved 
          ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→∀u:T.∀f:F.(pr3 c (THead (Flat f) u t1) (THead (Flat f) u t2))