DEFINITION pr2_ctail()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→∀k:K.∀u:T.(pr2 (CTail k u c) t1 t2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c t1 t2
        assume k: K
        assume u: T
          we proceed by induction on H to prove pr2 (CTail k u c) t1 t2
             case pr2_free : c0:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes pr2 (CTail k u c0) t3 t4
                   by (pr2_free . . . H0)
pr2 (CTail k u c0) t3 t4
             case pr2_delta : c0:C d:C u0:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u0) t3:T t4:T H1:pr0 t3 t4 t:T H2:subst0 i u0 t4 t ⇒
                the thesis becomes pr2 (CTail k u c0) t3 t
                   by (getl_ctail . . . . . H0 . .)
                   we proved getl i (CTail k u c0) (CHead (CTail k u d) (Bind Abbr) u0)
                   by (pr2_delta . . . . previous . . H1 . H2)
pr2 (CTail k u c0) t3 t
          we proved pr2 (CTail k u c) t1 t2
       we proved ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→∀k:K.∀u:T.(pr2 (CTail k u c) t1 t2)