proposition: Lemma list_pred_zip_l_eq : forall (A B: Set)(lsa : list A)(lsb : list B)(P : A -> B -> Prop), list_pred P lsa lsb -> list_pred (fun p a => (fst p) = a /\ P (fst p) (snd p)) (zip lsa lsb) lsa.
proof: Proof. intuition. eapply list_pred_impl. eapply list_pred_zip_l. eauto. eapply list_pred_eq. eapply list_pred_I. symmetry. eapply list_pred_length_eq; eauto. intuition. Qed.
imports: FCF.FCF