proposition: Lemma dot_cap_injective `{laws} `{AL ≪ l} {n m p} {x: X m n} {y z: X p m} {Hx: is_injective x}: (y ∩ z) ⋅ x ≡ (y⋅x) ∩ (z⋅x).
proof: Proof. revert Hx. dual @dot_univalent_cap. Qed.
imports: common lattice monoid kleene normalisation rewriting