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