proposition: Lemma functional_union : functional r -> functional r' -> (forall x, dom_rel r x -> dom_rel r' x -> False) -> functional (r ∪ r').
proof: Proof. unfold functional, union, dom_rel; ins; desf; eauto; try solve [exfalso; eauto]. Qed.
imports: HahnBase HahnList Relations