proposition: Lemma clean_weq l n m (x: expr n m): e_level x ≪ l -> clean x ==_[l] x.
proof: Proof. induction x; simpl e_level; simpl clean; try reflexivity; rewrite ?merge_spec; intuition. rewrite e_pls_weq. apply cup_weq; auto. rewrite 2clean_level. solve_lower'. rewrite e_dot_weq. apply dot_weq; auto. rewrite 2clean_level. solve_lower'. rewrite e_itr_weq. apply itr_weq; auto. rewrite clean_level. solve_lower'. rewrite e_str_weq. apply str_weq; auto. rewrite clean_level. solve_lower'. rewrite e_cnv_weq. apply cnv_weq; auto. rewrite clean_level. solve_lower'. Qed.
imports: kleene syntax