proposition: Theorem list_pred_impl' : forall (A B : Set) (lsa : list A) (lsb : list B) (P1 : A -> B -> Prop), list_pred P1 lsa lsb -> forall P2 : A -> B -> Prop, (forall (a : A) (b : B), In a lsa -> In b lsb -> P1 a b -> P2 a b) -> list_pred P2 lsa lsb.
proof: Proof. induction 1; intuition. econstructor. econstructor; intuition. Qed.
imports: FCF.FCF Permutation