\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b: B).(\forall
(v1: T).(\forall (v2: T).(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b)
v2)))))))
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b: B).(\forall
(v1: T).(\forall (v2: T).(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b)
v2)))))))