proposition: Lemma Choice : (forall x:S, {y:S' | R x y}) -> {f:S -> S' | forall z:S, R z (f z)}.
proof: Proof. intro H. exists (fun z => proj1_sig (H z)). intro z; destruct (H z); assumption. Defined.
imports: Notations Ltac Datatypes Logic