\forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall
(t2: T).((pr2 (CTail k u c) t1 t2) \to (or (pr2 c t1 t2) (ex3 T (\lambda (_:
T).(eq K k (Bind Abbr))) (\lambda (t: T).(pr0 t1 t)) (\lambda (t: T).(subst0
\forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall
(t2: T).((pr2 (CTail k u c) t1 t2) \to (or (pr2 c t1 t2) (ex3 T (\lambda (_:
T).(eq K k (Bind Abbr))) (\lambda (t: T).(pr0 t1 t)) (\lambda (t: T).(subst0