proposition: Lemma list_pred_map_r_eq : forall (A B : Set)(ls : list A)(f : A -> B), list_pred (fun a b => f a = b) ls (map f ls).
proof: Proof. induction ls; intuition; simpl in *. econstructor. econstructor; intuition. Qed.
imports: FCF.FCF