proposition: Lemma dom_to_doma : r ≡ ⦗d⦘ ⨾ r ⨾ ⦗d'⦘ -> doma r d.
proof: Proof. intro H; unfold doma; ins. hahn_rewrite H in REL; revert REL; basic_solver. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid