\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
B).(\forall (d1: C).(\forall (v1: T).((clear c1 (CHead d1 (Bind b1) v1)) \to
(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
B).(\forall (d1: C).(\forall (v1: T).((clear c1 (CHead d1 (Bind b1) v1)) \to
(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1