DEFINITION clear_pr2_trans()
TYPE =
       ∀c2:C.∀t1:T.∀t2:T.(pr2 c2 t1 t2)→∀c1:C.(clear c1 c2)→(pr2 c1 t1 t2)
BODY =
        assume c2: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c2 t1 t2
          we proceed by induction on H to prove ∀c1:C.(clear c1 c2)→(pr2 c1 t1 t2)
             case pr2_free : c:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes ∀c1:C.(clear c1 c)→(pr2 c1 t3 t4)
                    assume c1: C
                    suppose : clear c1 c
                      by (pr2_free . . . H0)
                      we proved pr2 c1 t3 t4
∀c1:C.(clear c1 c)→(pr2 c1 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 ∀c1:C.∀H3:(clear c1 c).(pr2 c1 t3 t)
                    assume c1: C
                    suppose H3: clear c1 c
                      by (clear_getl_trans . . . H0 . H3)
                      we proved getl i c1 (CHead d (Bind Abbr) u)
                      by (pr2_delta . . . . previous . . H1 . H2)
                      we proved pr2 c1 t3 t
∀c1:C.∀H3:(clear c1 c).(pr2 c1 t3 t)
          we proved ∀c1:C.(clear c1 c2)→(pr2 c1 t1 t2)
       we proved ∀c2:C.∀t1:T.∀t2:T.(pr2 c2 t1 t2)→∀c1:C.(clear c1 c2)→(pr2 c1 t1 t2)