proposition: Theorem list_pred_combine_l : forall (A B C : Set)P1 P2 (lsa : list A)(lsb : list B)(lsc : list C), list_pred P1 lsa lsc -> list_pred P2 lsb lsc -> list_pred (fun p c => P1 (fst p) c /\ P2 (snd p) c) (combine lsa lsb) lsc.
proof: Proof. intuition. eapply list_pred_combine_l_h; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation