\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).((drop n O
c2 e2) \to (or (drop n O c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n)
\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).((drop n O
c2 e2) \to (or (drop n O c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n)