proposition: Lemma dependent_choice : (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
proof: Proof. intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. split. - reflexivity. - intro n; induction n; simpl; apply proj2_sig. Defined.
imports: Notations Ltac Datatypes Logic