proposition: Lemma laws `{monoid.laws} `{BKA ≪ l}: kat.laws (ops X).
proof: Proof. constructor. apply lower_laws. intro. apply lower_lattice_laws. intro. constructor; try discriminate. apply ofbool_leq. apply op_leq_weq_1. intros _ ? ?. apply orb_pls. intros _. reflexivity. intros ?. reflexivity. intros ? ? ?. apply andb_dot. Qed.
imports: boolean ugregex_dec kat_reification kat_untyping kat_completeness