proposition: Lemma eval_erase: forall n m (x: expr n m), is_clean x -> eval n m (erase x) x.
proof: Proof. induction x; simpl (is_clean _); intro Hl; try discriminate Hl; try constructor; first [apply IHx1 | apply IHx2 | apply IHx | idtac]; tauto. Qed.
imports: kleene syntax