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