proposition: Lemma Forall_dec : (forall x:A, {P x} + { ~ P x }) -> forall l:list A, {Forall l} + {~ Forall l}.
proof: Proof. intros Pdec l. induction l as [|a l' Hrec]. - left. apply Forall_nil. - destruct Hrec as [Hl'|Hl']. + destruct (Pdec a) as [Ha|Ha]. * left. now apply Forall_cons. * right. abstract now inversion 1. + right. abstract now inversion 1. Defined.
imports: PeanoNat