proposition: Lemma pls'pls: forall l n m (x y: expr n m) {Hl: CUP+e_level x+e_level y ≪ l}, pls' x y ==_[l] x+y.
proof: Proof. induction x; simpl e_level; simpl pls'; intros y Hl; try (subst; now rewrite insert_pls_pls by solve_lower'). lattice. lattice. rewrite insert_pls_pls, IHx1 by (rewrite ?pls'_level; solve_lower'). lattice. Qed.
imports: kleene syntax powerfix