proposition: Lemma list_dec_all : forall (l : list A), (forall x, In x l -> {P x} + {~P x}) -> {forall x, In x l -> P x} + {exists x, In x l /\ ~P x}.
proof: Proof. induction l; intros. left; intros; inversion H. destruct (IHl). intros; apply X. auto with datatypes. destruct (X a). auto with datatypes. left; intros; inversion H. rewrite <- H0; trivial. apply p; trivial. right; exists a; split; auto with datatypes. right. destruct e as [x [x_l nPx]]. exists x; split; auto with datatypes. Defined.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)