proposition: Lemma doma_helper : r ⊆ ⦗d⦘ ⨾ r <-> doma r d.
proof: Proof. split; unfold doma, inclusion, seq, eqv_rel; ins; desf. by apply H in REL; desf. by eexists; splits; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid