proposition: Lemma countable_choice' : forall (T U : Type) F, (forall x : nat, exists X : T -> U, F x X) -> exists Z, forall x : nat, F x (Z x).
proof: Proof. intros T U F H. destruct (countable_choice T U F) as [Z HZ]. exists Z. intro x. apply HZ. apply H. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers