\forall (c1: C).(\forall (d1: C).((clear c1 d1) \to (\forall (g: G).(\forall
(d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda
(c2: C).(clear c2 d2))))))))
\forall (c1: C).(\forall (d1: C).((clear c1 d1) \to (\forall (g: G).(\forall
(d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda
(c2: C).(clear c2 d2))))))))