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 =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c t1 t2
        assume u: T
        assume f: F
          we proceed by induction on H to prove pr2 c (THead (Flat f) u t1) (THead (Flat f) u t2)
             case pr2_free : c0:C t0:T t3:T H0:pr0 t0 t3 ⇒
                the thesis becomes pr2 c0 (THead (Flat f) u t0) (THead (Flat f) u t3)
                   by (pr0_refl .)
                   we proved pr0 u u
                   by (pr0_comp . . previous . . H0 .)
                   we proved pr0 (THead (Flat f) u t0) (THead (Flat f) u t3)
                   by (pr2_free . . . previous)
pr2 c0 (THead (Flat f) u t0) (THead (Flat f) u t3)
             case pr2_delta : c0:C d:C u0:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u0) t0:T t3:T H1:pr0 t0 t3 t:T H2:subst0 i u0 t3 t ⇒
                the thesis becomes pr2 c0 (THead (Flat f) u t0) (THead (Flat f) u t)
                   (h1) 
                      by (pr0_refl .)
                      we proved pr0 u u
                      by (pr0_comp . . previous . . H1 .)
pr0 (THead (Flat f) u t0) (THead (Flat f) u t3)
                   end of h1
                   (h2) 
                      consider H2
                      we proved subst0 i u0 t3 t
                      that is equivalent to subst0 (s (Flat f) i) u0 t3 t
                      by (subst0_snd . . . . . previous .)
subst0 i u0 (THead (Flat f) u t3) (THead (Flat f) u t)
                   end of h2
                   by (pr2_delta . . . . H0 . . h1 . h2)
pr2 c0 (THead (Flat f) u t0) (THead (Flat f) u t)
          we proved pr2 c (THead (Flat f) u t1) (THead (Flat f) u t2)
       we proved 
          ∀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))