proposition: Lemma kernel_refl_antisym `{laws} `{CAP+CNV ≪ l} {n} {x: X n n} {Hr: is_reflexive x} {Ha: is_antisymmetric x}: x° ⊓ x ≡ 1.
proof: Proof. apply antisym. assumption. apply cap_spec; split; trivial. now rewrite <-reflexive. Qed.
imports: common lattice monoid kleene normalisation rewriting