proposition: Lemma functionalE : functional r -> exists f, forall x y, r x y <-> f x = Some y.
proof: Proof. clear; unfold functional; ins. forward apply unique_choice with (R := fun x y => y = None /\ ~ (exists m, r x m) \/ exists m, y = Some m /\ r x m) as X; ins; desf. by tertium_non_datur (exists m, r x m); desc; [exists (Some m)| exists None]; split; ins; desf; try f_equal; eauto; try solve [exfalso; eauto]. exists f; ins; specialize (X x); split; ins; desf; try solve [exfalso; eauto]. rewrite X; f_equal; eauto. Qed.
imports: HahnBase HahnList Relations