DEFINITION clear_gen_bind()
TYPE =
       ∀b:B
         .∀e:C
           .∀x:C
             .∀u:T
               .clear (CHead e (Bind b) u) x
                 →eq C x (CHead e (Bind b) u)
BODY =
Show proof