proposition: Lemma clean_idem n m (e: expr n m): clean (clean e) = clean e.
proof: Proof. induction e; simpl; trivial; destruct_tests; intros; simpl; rewrite ?IHe1, ?IHe2, ?IHe; destruct_tests; congruence. Qed.
imports: kleene syntax