proposition: Lemma Forall_Exists_dec (P:A->Prop) : (forall x:A, {P x} + { ~ P x }) -> forall l:list A, {Forall P l} + {Exists (fun x => ~ P x) l}.
proof: Proof. intros Pdec l. destruct (Forall_dec P Pdec l); [left|right]; trivial. now apply neg_Forall_Exists_neg. Defined.
imports: PeanoNat