proposition: Lemma rmov_x_pls `{L: monoid.laws} `{Hl: CUP ≪ l} {n m} x y (e f: X n m): x;e ≡ e;y -> x;f ≡ f;y -> x;(e+f) ≡ (e+f);y.
proof: Proof. intros. ra_normalise. now apply cup_weq. Qed.
imports: kat normalisation rewriting kat_tac