\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TLRef n) x) \to
(or (eq T x (TLRef n)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl n c
(CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T x (lift (S
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TLRef n) x) \to
(or (eq T x (TLRef n)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl n c
(CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T x (lift (S