proposition: Lemma norm_level n m (x: expr n m): e_level (norm x) ≪ e_level x.
proof: Proof. induction x; simpl norm; simpl e_level; rewrite ?dot'_level, ?pls'_level, ?cap'_level, ?cnv'_level, ?itr'_level, ?str'_level, ?IHx1, ?IHx2, ?IHx; solve_lower'. Qed.
imports: kleene syntax powerfix