DEFINITION clear_gen_flat_r()
TYPE =
       ∀f:F.∀x:C.∀e:C.∀u:T.(clear x (CHead e (Flat f) u))→∀P:Prop.P
BODY =
Show proof