proposition: Lemma domab_helper : r ⊆ ⦗d⦘ ⨾ r ⨾ ⦗d'⦘ <-> doma r d /\ domb r d'.
proof: Proof. split; ins; splits; unfold doma, domb, inclusion, eqv_rel, seq in *; ins; desf; try specialize (H _ _ REL); try specialize (H1 _ _ H0); desf; splits; eexists; splits; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid