(x: C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(ex_intro2 C
(\lambda (c2: C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2
d2)) x (wf3_flat g e x H4 u f) H5)))) H3)))))))))))) c1 d1 H))).
(x: C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(ex_intro2 C
(\lambda (c2: C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2
d2)) x (wf3_flat g e x H4 u f) H5)))) H3)))))))))))) c1 d1 H))).