proposition: Lemma list_pred_map_l : forall (A B : Set) (lsa : list A) (lsb : list B) (P : A -> B -> Prop), list_pred P lsa lsb -> forall (C : Set) (f : A -> C), list_pred (fun (c : C) (b : B) => exists a : A, P a b /\ c = f a) (map f lsa) lsb.
proof: Proof. induction 1; intuition; simpl in *. econstructor. econstructor. econstructor; eauto. eauto. Qed.
imports: FCF.FCF Permutation