proposition: Theorem list_pred_combine_l_h : forall (A C : Set)(lsa : list A)(lsc : list C) P1, list_pred P1 lsa lsc -> forall (B : Set)(lsb : list B) P2, list_pred P2 lsb lsc -> list_pred (fun p c => P1 (fst p) c /\ P2 (snd p) c) (combine lsa lsb) lsc.
proof: Proof. induction 1; intuition; simpl in *. econstructor. inversion H1; clear H1; subst. econstructor. intuition. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation