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