proposition: Lemma dot_l_level n m p (x: expr n m) (y: expr m p): e_level (dot_l x y) ≪ e_level x + e_level y.
proof: Proof. revert p y. induction x; intros q z; simpl dot_l; case_distribute; simpl e_level; rewrite ?pls'_level, ?IHx1, ?IHx2; solve_lower'. Qed.
imports: kleene syntax powerfix