proposition: Theorem contrapositive_countable_choice : forall e, λ"x" "x" @ quote'↓e ⊩ ∀F, ∃U, ∀x : nat, ((∀₁n∈ℕ, F x (U x n)) → ∀X : nat -> formula, F x X).
proof: Proof. Kmove. destruct (quote'_realizer F) as [U HU]. find. apply HU. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers