proposition: Lemma exlist_dec : forall (A : Set) (P : A -> Prop) (l : list A), (forall x : A, P x \/ ~ P x) -> exlist A P l \/ ~ exlist A P l.
proof: Proof. simple induction l. simpl in |- *. right. intro. assumption. intros h t IH H. simpl in |- *. elim (H h). left. left. assumption. elim IH. left. right. assumption. right. intro. elim H2. assumption. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ