DEFINITION csubt_pr2()
TYPE =
       ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pr2 c1 t1 t2)→∀c2:C.(csubt g c1 c2)→(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.(csubt g c1 c2)→(pr2 c2 t1 t2)
             case pr2_free : c:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes ∀c2:C.(csubt g c c2)→(pr2 c2 t3 t4)
                    assume c2: C
                    suppose : csubt g c c2
                      by (pr2_free . . . H0)
                      we proved pr2 c2 t3 t4
∀c2:C.(csubt g c c2)→(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:(csubt g c c2).(pr2 c2 t3 t)
                    assume c2: C
                    suppose H3: csubt g c c2
                      (H4) 
                         by (csubt_getl_abbr . . . . . H0 . H3)
ex2 C λd2:C.csubt g d d2 λd2:C.getl i c2 (CHead d2 (Bind Abbr) u)
                      end of H4
                      we proceed by induction on H4 to prove pr2 c2 t3 t
                         case ex_intro2 : x:C :csubt g d x H6:getl i c2 (CHead x (Bind Abbr) u) ⇒
                            the thesis becomes pr2 c2 t3 t
                               by (pr2_delta . . . . H6 . . H1 . H2)
pr2 c2 t3 t
                      we proved pr2 c2 t3 t
∀c2:C.∀H3:(csubt g c c2).(pr2 c2 t3 t)
          we proved ∀c2:C.(csubt g c1 c2)→(pr2 c2 t1 t2)
       we proved ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pr2 c1 t1 t2)→∀c2:C.(csubt g c1 c2)→(pr2 c2 t1 t2)