proposition: Lemma univalent_antisym `{AL+TOP ≪ l} {n m} {x y: X n m} {Hy: is_univalent y}: y⋅top' m m ≦ x⋅top -> x ≦ y -> x ≡ y.
proof: Proof. intros Ht Hxy. apply antisym. assumption. transitivity (y ⊓ (x⋅(top' m m))). rewrite <- Ht, <- dotxt. lattice. rewrite capC, capdotx. ra_normalise. rewrite Hxy at 2. mrewrite univalent. ra. Qed.
imports: common lattice monoid kleene normalisation rewriting