DEFINITION wf3_pr3_conf()
TYPE =
       ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pr3 c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr3 c2 t1 t2)
BODY =
        assume g: G
        assume c1: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c1 t1 t2
          we proceed by induction on H to prove ∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr3 c2 t1 t2)
             case pr3_refl : t:T ⇒
                the thesis becomes ∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t u)→(pr3 c2 t t)
                    assume c2: C
                    suppose : wf3 g c1 c2
                    assume u: T
                    suppose : ty3 g c1 t u
                      by (pr3_refl . .)
                      we proved pr3 c2 t t
∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t u)→(pr3 c2 t t)
             case pr3_sing : t3:T t4:T H0:pr2 c1 t4 t3 t5:T :pr3 c1 t3 t5 ⇒
                the thesis becomes ∀c2:C.∀H3:(wf3 g c1 c2).∀u:T.∀H4:(ty3 g c1 t4 u).(pr3 c2 t4 t5)
                (H2) by induction hypothesis we know ∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t3 u)→(pr3 c2 t3 t5)
                    assume c2: C
                    suppose H3: wf3 g c1 c2
                    assume u: T
                    suppose H4: ty3 g c1 t4 u
                      (h1) 
                         by (wf3_pr2_conf . . . . H0 . H3 . H4)
pr2 c2 t4 t3
                      end of h1
                      (h2) 
                         by (ty3_sred_pr2 . . . H0 . . H4)
                         we proved ty3 g c1 t3 u
                         by (H2 . H3 . previous)
pr3 c2 t3 t5
                      end of h2
                      by (pr3_sing . . . h1 . h2)
                      we proved pr3 c2 t4 t5
∀c2:C.∀H3:(wf3 g c1 c2).∀u:T.∀H4:(ty3 g c1 t4 u).(pr3 c2 t4 t5)
          we proved ∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr3 c2 t1 t2)
       we proved ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pr3 c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr3 c2 t1 t2)