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