DEFINITION wf3_pr2_conf()
TYPE =
       ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pr2 c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr2 c2 t1 t2)
BODY =
        assume g: G
        assume c1: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c1 t1 t2
          we proceed by induction on H to prove ∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr2 c2 t1 t2)
             case pr2_free : c:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes ∀c2:C.(wf3 g c c2)→∀u:T.(ty3 g c t3 u)→(pr2 c2 t3 t4)
                    assume c2: C
                    suppose : wf3 g c c2
                    assume u: T
                    suppose : ty3 g c t3 u
                      by (pr2_free . . . H0)
                      we proved pr2 c2 t3 t4
∀c2:C.(wf3 g c c2)→∀u:T.(ty3 g c t3 u)→(pr2 c2 t3 t4)
             case pr2_delta : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) t3:T t4:T H1:pr0 t3 t4 t:T H2:subst0 i u t4 t ⇒
                the thesis becomes ∀c2:C.∀H3:(wf3 g c c2).∀u0:T.∀H4:(ty3 g c t3 u0).(pr2 c2 t3 t)
                    assume c2: C
                    suppose H3: wf3 g c c2
                    assume u0: T
                    suppose H4: ty3 g c t3 u0
                      (H_y) by (ty3_sred_pr0 . . H1 . . . H4) we proved ty3 g c t4 u0
                      (H_x) 
                         by (ty3_getl_subst0 . . . . H_y . . . H2 . . . H0)
ex T λw:T.ty3 g d u w
                      end of H_x
                      (H5) consider H_x
                      we proceed by induction on H5 to prove pr2 c2 t3 t
                         case ex_intro : x:T H6:ty3 g d u x ⇒
                            the thesis becomes pr2 c2 t3 t
                               (H_x0) 
                                  by (wf3_getl_conf . . . . . H0 . . H3 . H6)
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.wf3 g d d2
                               end of H_x0
                               (H7) consider H_x0
                               we proceed by induction on H7 to prove pr2 c2 t3 t
                                  case ex_intro2 : x0:C H8:getl i c2 (CHead x0 (Bind Abbr) u) :wf3 g d x0 ⇒
                                     the thesis becomes pr2 c2 t3 t
                                        by (pr2_delta . . . . H8 . . H1 . H2)
pr2 c2 t3 t
pr2 c2 t3 t
                      we proved pr2 c2 t3 t
∀c2:C.∀H3:(wf3 g c c2).∀u0:T.∀H4:(ty3 g c t3 u0).(pr2 c2 t3 t)
          we proved ∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr2 c2 t1 t2)
       we proved ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pr2 c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→∀u:T.(ty3 g c1 t1 u)→(pr2 c2 t1 t2)