proposition: Lemma dot_univalent_cap `{AL ≪ l} {n m p} {x: X n m} {y z: X m p} {E: is_univalent x}: x ⋅ (y ∩ z) ≡ (x⋅y) ∩ (x⋅z).
proof: Proof. apply antisym. ra. rewrite capdotx. mrewrite univalent. ra. Qed.
imports: common lattice monoid kleene normalisation rewriting