proposition: Lemma Forall_and : forall (P Q : A -> Prop) l, Forall P l -> Forall Q l -> Forall (fun x => P x /\ Q x) l.
proof: Proof. intros P Q l; induction l; intros HP HQ; constructor; inversion HP; inversion HQ; auto. Qed.
imports: PeanoNat