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