\forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall
(v: T).((csubst0 i v c1 c2) \to (\forall (u: T).(csubst0 (S i) v (CHead c1
(Bind b) u) (CHead c2 (Bind b) u))))))))
\forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall
(v: T).((csubst0 i v c1 c2) \to (\forall (u: T).(csubst0 (S i) v (CHead c1
(Bind b) u) (CHead c2 (Bind b) u))))))))