proposition: Lemma bool_choice : (forall x:S, {R1 x} + {R2 x}) -> {f:S -> bool | forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
proof: Proof. intro H. exists (fun z:S => if H z then true else false). intro z; destruct (H z); auto. Defined.
imports: Notations Ltac Datatypes Logic