proposition: Theorem countable_surj : Countable A <-> exists R, rel_enumerates R.
proof: Proof. split. - intros [f Hf]. exists (fun (n : nat) (x : U) => exists H : In A x, f (exist _ x H) = n). split. + intros n x _ [Hx0 Hx1]. apply Hx0. + intros n x y _ [Hx0 Hx1] [Hy0 Hy1]. subst. apply Hf in Hy1. inversion Hy1; subst; clear Hy1. reflexivity. + intros x H. exists (f (exist _ x H)). split; [constructor|]. exists H. reflexivity. - intros [R HR]. assert ( forall p : { x : U | In A x }, exists ! x : nat, R x (proj1_sig p) /\ (forall m : nat, R m (proj1_sig p) -> (x <= m)%nat)) as Hrel. { destruct HR as [HR0 HR1 HR2]. intros p. pose proof (WF_implies_MEP nat _ lt_wf_0 (fun n : nat => R n (proj1_sig p)) ) as Hwf. specialize (HR2 (proj1_sig p) (proj2_sig p)) as [n' [_ Hn']]. destruct Hwf as [n [Hn0 Hn1]]. { exists n'. assumption. } clear n' Hn'. exists n. split; [split|]. * assumption. * intros m Hm. specialize (Hn1 m Hm). lia. * intros m [Hm0 Hm1]. specialize (Hn1 m Hm0). specialize (Hm1 n Hn0). lia. } exists (fun p : { x : U | In A x } => proj1_sig (constructive_definite_description _ (Hrel p))). intros p0 p1 Hp. pose proof (proj2_sig (constructive_definite_description _ (Hrel p0))) as [Hp0 _]. pose proof (proj2_sig (constructive_definite_description _ (Hrel p1))) as [Hp1 _]. rewrite Hp in Hp0. destruct HR as [_ HR _]. specialize (HR _ _ _ ltac:(constructor) Hp0 Hp1). clear Hp Hp0 Hp1 Hrel. destruct p0 as [? H0], p1 as [? H1]. simpl in HR. subst. destruct (proof_irrelevance _ H0 H1). reflexivity. Qed.
imports: Coq(Ensembles Arith ArithRing Wellfounded Relations Wf_nat Finite_sets Logic.Epsilon Sets.Image Lia) ZornsLemma(Classical_Wf CountableTypes Families) hydras(MoreEpsilonIota PartialFun GRelations Prelude.More_Arith)