proposition: Lemma dom_union : dom_rel (r ∪ r') ≡₁ dom_rel r ∪₁ dom_rel r'.
proof: Proof. unfold dom_rel, union, set_union, set_equiv, set_subset. split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid