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