proposition: Lemma pls'x0 n m (x: expr n m) l `{CUP+e_level x ≪ l}: pls' x 0 ==_[l] x.
proof: Proof. induction x; try reflexivity. simpl pls'. simpl e_level in *. rewrite insert_pls_pls, IHx1. apply cupC. solve_lower'. rewrite pls'x0_level. solve_lower'. Qed.
imports: kleene syntax powerfix