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