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