proposition: Lemma list_pred_zip_r : forall (A B: Set)(lsa : list A)(lsb : list B)(P : A -> B -> Prop), list_pred P lsa lsb -> forall (C : Set)(lsc : list C)(P1 : A -> C -> Prop)(P2 : B -> C -> Prop), list_pred P1 lsa lsc -> list_pred P2 lsb lsc -> list_pred (fun c (p : A * B) => P (fst p) (snd p) /\ P1 (fst p) c /\ P2 (snd p) c) lsc (zip lsa lsb).
proof: Proof. induction 1; intuition. inversion H. subst. econstructor. inversion H1; clear H1; subst. inversion H2; clear H2; subst. simpl. econstructor; intuition. Qed.
imports: FCF.FCF