proposition: Lemma insert_pls_level n m (x y: expr n m): e_level (insert_pls x y) ≪ CUP+e_level x+e_level y.
proof: Proof. induction x; simpl; try case cmp_spec; simpl e_level; intros; try solve_lower'. rewrite IHx1. solve_lower'. Qed.
imports: kleene syntax powerfix