proposition: Lemma map_eq : forall (A B C : Set)(lsa : list A)(lsb : list B)(f1 : A -> C)(f2 : B -> C), list_pred (fun a b => f1 a = f2 b) lsa lsb -> map f1 lsa = map f2 lsb.
proof: Proof. induction lsa; inversion 1; intuition; simpl in *; subst. f_equal; eauto. Qed.
imports: FCF.FCF Permutation