proposition: Lemma insert_pls_pls: forall l n m (x y: expr n m) {Hl: CUP+e_level x ≪ l}, insert_pls x y ==_[l] y+x.
proof: Proof. assert (D: forall n m (x y: expr n m) l, CUP+e_level x ≪ l -> y+x ==_[l] match cmp x y with Lt => x+y | Gt => y+x | Eq => y end). intros. case cmp_spec; intros; try subst; lattice. intros; symmetry; induction x; simpl e_level in *; try (apply D; solve_lower). lattice. lattice. simpl insert_pls. case cmp_spec; intros. subst. lattice. fold_expr l. rewrite <- IHx1 by solve_lower'. lattice. lattice. Qed.
imports: kleene syntax powerfix