proposition: Lemma clean_level n m (x: expr n m): e_level (clean x) ≪ e_level x.
proof: Proof. induction x; try reflexivity; simpl clean; revert_prop; destruct_tests; simpl e_level; intros; solve_lower' || reflexivity. Qed.
imports: kleene syntax