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