INDUCTIVE DEFINITION clear () [ ]
OF ARITY C→C→Prop
BUILT FROM:
     clear_bind: ∀b:B.∀e:C.∀u:T.(clear (CHead e (Bind b) u) (CHead e (Bind b) u))
   | clear_flat: ∀e:C.∀c:C.(clear e c)→∀f:F.∀u:T.(clear (CHead e (Flat f) u) c)