proposition: Lemma map_f_equal : forall (A B : Type)(f1 f2 : A -> B)(ls1 ls2 : list A), (forall a, f1 a = f2 a) -> ls1 = ls2 -> map f1 ls1 = map f2 ls2.
proof: Proof. intuition. subst. eapply map_ext. trivial. Qed.
imports: FCF.FCF Permutation