proposition: Lemma exists_in_list_dec : forall l, {exists r, P r /\ In r l} + {~exists r, P r /\ In r l}.
proof: Proof. induction l. right. intuition. do 2 destruct H; simpl in H; auto. destruct (P_dec a). left; exists a; simpl; auto. destruct IHl. left. destruct e. exists x. simpl; tauto. right; intuition. do 2 destruct H. simpl in H0. destruct H0. subst; tauto. apply n0. exists x; auto. Defined.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)