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