proposition: Lemma rmov_x_dot `{L: monoid.laws} {n m p} x y z (e: X n m) (f: X m p): x;e ≡ e;y -> y;f ≡ f;z -> x;(e;f) ≡ (e;f);z.
proof: Proof. intros He Hf. rewrite dotA, He, <-dotA, Hf. apply dotA. Qed.
imports: kat normalisation rewriting kat_tac