proposition: Lemma dot_l_weq l n m p (x: expr n m) (y: expr m p) {Hl: e_level x + e_level y ≪ l}: x⋅y ==_[l] dot_l x y.
proof: Proof. revert p y Hl. induction x; intros q z Hl; simpl dot_l; case_distribute; simpl e_level in Hl; try reflexivity. apply dot0x. apply dot1x. now rewrite dotplsx, pls'pls, <-IHx1, <-IHx2 by (rewrite ?dot_l_level; solve_lower'). Qed.
imports: kleene syntax powerfix