proposition: Theorem Forall2_impl : forall (A B : Type)(lsa : list A)(lsb : list B) (P1 P2 : A -> B -> Prop), Forall2 P1 lsa lsb -> (forall a b, P1 a b -> P2 a b) -> Forall2 P2 lsa lsb.
proof: Proof. induction 1; intuition idtac. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation