proposition: Lemma eq_dom_union : eq_dom (d ∪₁ d') f g <-> eq_dom d f g /\ eq_dom d' f g.
proof: Proof. split. { ins. unfold eq_dom in *. splits; ins; apply (H x); basic_solver. } intros [Hs Hs']. unfold eq_dom in *. ins. unfold set_union in DX. desf; basic_solver. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid