proposition: Lemma list_pred_zip_in : forall (A B : Set)(P : A -> B -> Prop)(lsa : list A)(lsb : list B), list_pred P lsa lsb -> forall a b, In (a, b) (zip lsa lsb) -> P a b.
proof: Proof. induction 1; intuition; simpl in *. intuition. intuition. pairInv. trivial. Qed.
imports: FCF.FCF Permutation