proposition: Theorem AC_realizer : forall F, exists V, forall (x : nat) e, AC↓e ⊩ (∀X, (∀y : nat, (V x y → X y)) → (∀y : nat, (X y → V x y)) → F x X) → ∀X, F x X.
proof: Proof. intro F. destruct (quote'_realizer F) as [U HU]. assert (forall x e, Y↓e ⊩ (∀n, (∀m, m < n ↦ {Z.of_nat m} → F x (U x m)) → {Z.of_nat n} → F x (U x n)) → ∀₁n∈ℕ, F x (U x n)) as Y_realizer_F. intros. startn 0. fold Y. apply (Y_realizer Wf_nat.lt_wf). find. now apply Ht. find. pose (V x y := ∀n, (∀m, m < n ↦ {Z.of_nat m} → F x (U x m)) → {Z.of_nat n} → (¬(F x (U x n))) → U x n y). exists V. intros x e. Ksolve. apply HU. find. Kmove. eapply Y_realizer_F. find. Ksolve. now do 2 Ksolve. unfold V. Ksolve. eapply comp_realizer. find. now Ksolve. Ksolve. now subst. now do 2 Ksolve. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers