\forall (i: nat).(\forall (n: nat).((lt n i) \to (\forall (c1: C).(\forall
(c2: C).(\forall (v: T).((csubst1 i v c1 c2) \to (\forall (e1: C).((getl n c1
e1) \to (ex2 C (\lambda (e2: C).(csubst1 (minus i n) v e1 e2)) (\lambda (e2:
\forall (i: nat).(\forall (n: nat).((lt n i) \to (\forall (c1: C).(\forall
(c2: C).(\forall (v: T).((csubst1 i v c1 c2) \to (\forall (e1: C).((getl n c1
e1) \to (ex2 C (\lambda (e2: C).(csubst1 (minus i n) v e1 e2)) (\lambda (e2: