proposition: Lemma dom_cross (N: ~ d' ≡₁ ∅): dom_rel (d × d') ≡₁ d.
proof: Proof. apply set_nonemptyE in N; unfold dom_rel, cross_rel, set_equiv, set_subset; split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid