proposition: Lemma many_one_dec : forall (l : list A) r, (forall x, In x l -> {R x r} + {~R x r}) -> {x : A | In x l /\ R x r} + {forall x, In x l -> ~R x r}.
proof: Proof. induction l; intros. right; intros. inversion H. destruct (X a); auto with datatypes. left; exists a; auto with datatypes. case (IHl r); intro. intros; apply X; auto with datatypes. left. destruct s as [x [x_l x_r]]. exists x; auto with datatypes. right. intros. destruct H. rewrite <- H; trivial. apply n0; trivial. Defined.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)