proposition: Lemma Forall_and_inv : forall (P Q : A -> Prop) l, Forall (fun x => P x /\ Q x) l -> Forall P l /\ Forall Q l.
proof: Proof. intros P Q l; induction l; intro Hl; split; constructor; inversion Hl; firstorder. Qed.
imports: PeanoNat