proposition: Theorem list_pred_map_both': forall (A B C D : Set) (lsa : list A) (lsb : list B) (P : C -> D -> Prop) (f : A -> C)(g : B -> D), list_pred (fun (a : A) (b : B) => P (f a) (g b)) lsa lsb -> list_pred P (map f lsa) (map g lsb).
proof: Proof. intuition. eapply list_pred_impl. eapply list_pred_map_both. eauto. intuition. destruct H0. destruct H0. intuition; subst. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation