proposition: Lemma Choice2 : (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 => projT1 (H z)). intro z; destruct (H z); assumption. Defined.
imports: Notations Ltac Datatypes Logic