DEFINITION pr2_gen_ctail()
TYPE =
       ∀k:K
         .∀c:C
           .∀u:T
             .∀t1:T
               .∀t2:T
                 .pr2 (CTail k u c) t1 t2
                   →or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c) u t t2)
BODY =
Show proof