proposition: Lemma domab_helper2 : r ⊆ d × d' <-> doma r d /\ domb r d'.
proof: Proof. unfold doma, domb, cross_rel, inclusion; intuition; firstorder. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid