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 =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pc3 c t1 t2
        assume u: T
        assume f: F
          (H0) consider H
          consider H0
          we proved pc3 c t1 t2
          that is equivalent to ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t
          we proceed by induction on the previous result to prove pc3 c (THead (Flat f) u t1) (THead (Flat f) u t2)
             case ex_intro2 : x:T H1:pr3 c t1 x H2:pr3 c t2 x ⇒
                the thesis becomes pc3 c (THead (Flat f) u t1) (THead (Flat f) u t2)
                   (h1) 
                      by (pr3_thin_dx . . . H1 . .)
pr3 c (THead (Flat f) u t1) (THead (Flat f) u x)
                   end of h1
                   (h2) 
                      by (pr3_thin_dx . . . H2 . .)
pr3 c (THead (Flat f) u t2) (THead (Flat f) u x)
                   end of h2
                   by (ex_intro2 . . . . h1 h2)
                   we proved ex2 T λt:T.pr3 c (THead (Flat f) u t1) t λt:T.pr3 c (THead (Flat f) u t2) t
pc3 c (THead (Flat f) u t1) (THead (Flat f) u t2)
          we proved pc3 c (THead (Flat f) u t1) (THead (Flat f) u t2)
       we proved 
          ∀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))