proposition: Lemma list_pred_map_r' : forall (A B C : Set) (lsa : list A) (lsb : list B) (P : A -> C -> Prop) (f : B -> C), list_pred (fun a b => P a (f b)) lsa lsb -> list_pred P lsa (map f lsb).
proof: Proof. induction lsa; inversion 1; intuition; subst; simpl in *; econstructor. inversion H; clear H; subst. trivial. eauto. Qed.
imports: FCF.FCF Permutation