\forall (c: C).(\forall (e: C).(\forall (v: T).(\forall (i: nat).((getl i c
(CHead e (Bind Abbr) v)) \to (\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2)
\to (\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr3 c
\forall (c: C).(\forall (e: C).(\forall (v: T).(\forall (i: nat).((getl i c
(CHead e (Bind Abbr) v)) \to (\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2)
\to (\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr3 c