proposition: Lemma dot'dot l n m p (x: expr n m) (y: expr m p) {Hl: e_level y+e_level x ≪ l}: dot' x y ==_[l] x⋅y.
proof: Proof. symmetry. unfold dot'. revert n x Hl. induction y; simpl e_level; intros q z Hl; simpl dot_r; case_distribute; try reflexivity; try (apply dot_l_weq; solve_lower'). apply dotx0. apply dotx1. now rewrite dotxpls, pls'pls, <-IHy1, <-IHy2 by (rewrite ?dot_r_level; solve_lower'). now rewrite <-dot_l_weq, <-IHy1, dotA by (rewrite ?dot_r_level; solve_lower'). Qed.
imports: kleene syntax powerfix