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