proposition: Lemma clean_erase h k n m (e: expr n m): clean (erase h e) = erase k (clean e).
proof: Proof. induction e; simpl; unfold e_pls', e_dot', e_itr', e_str', e_pls', e_cnv'; simpl in *; trivial; rewrite ?IHe1, ?IHe2, ?IHe, ?is_zer_erase; repeat (case is_zer; trivial). Qed.
imports: kleene syntax