DEFINITION clear_gen_all()
TYPE =
       ∀c1:C.∀c2:C.(clear c1 c2)→(ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u))
BODY =
Show proof