proposition: Theorem quote'_realizer : forall (F : nat -> (nat -> formula) -> formula), exists U : nat -> nat -> nat -> formula, forall e, quote' ↓e ⊩ ∀x, (∀₁n∈ℕ, F x (U x n)) → ∀X, F x X.
proof: Proof. intro F. assert (forall x π, exists R, π ∈ ‖∀X, F x X‖ <-> π ∈ ‖F x R‖) as Hc. intros x π. apply NNPP. intro Habs. apply Habs. exists (fun _ => ⊤). split. intros [R Hπ]. exfalso. apply Habs. exists R. split; intro; now try exists R. intro. find. assert (forall xπ, exists R, Penum (p2 xπ) ∈ ‖∀X, F (p1 xπ) X‖ <-> Penum (p2 xπ) ∈ ‖F (p1 xπ) R‖) as Hc'. intro xπ. apply Hc. assert (exists U, forall x π, π ∈ ‖∀X, F x X‖ <-> π ∈ ‖F x (U x (enumP π))‖) as HU. apply (countable_choice' nat formula (fun xπ R => (Penum (p2 xπ)) ∈ ‖∀X : nat -> formula, F (p1 xπ) X‖ <-> (Penum (p2 xπ)) ∈ ‖F (p1 xπ) R‖)) in Hc'. destruct Hc' as [U' HU]. exists (fun x nπ => U' (pair x nπ)). intros x π. pose (xπ := pair x (enumP π)). fold xπ. rewrite <- (enumP_Penum π). rewrite <-(p2_pair x (enumP π)). fold xπ. rewrite <- (p1_pair x (enumP π)). fold xπ. apply HU. destruct HU as [U HU]. exists U. Ksolve. apply anti_evaluation with (t ★ Int(Z.of_nat (enumP π))↓∅·π). now apply red_quote'. Ksolve. rewrite <- HU. find. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers