DEFINITION clear_pr3_trans()
TYPE =
       ∀c2:C.∀t1:T.∀t2:T.(pr3 c2 t1 t2)→∀c1:C.(clear c1 c2)→(pr3 c1 t1 t2)
BODY =
        assume c2: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c2 t1 t2
        assume c1: C
        suppose H0: clear c1 c2
          we proceed by induction on H to prove pr3 c1 t1 t2
             case pr3_refl : t:T ⇒
                the thesis becomes pr3 c1 t t
                   by (pr3_refl . .)
pr3 c1 t t
             case pr3_sing : t3:T t4:T H1:pr2 c2 t4 t3 t5:T :pr3 c2 t3 t5 ⇒
                the thesis becomes pr3 c1 t4 t5
                (H3) by induction hypothesis we know pr3 c1 t3 t5
                   by (clear_pr2_trans . . . H1 . H0)
                   we proved pr2 c1 t4 t3
                   by (pr3_sing . . . previous . H3)
pr3 c1 t4 t5
          we proved pr3 c1 t1 t2
       we proved ∀c2:C.∀t1:T.∀t2:T.(pr3 c2 t1 t2)→∀c1:C.(clear c1 c2)→(pr3 c1 t1 t2)