proposition: Theorem map_pair_fst_eq : forall (A B C D: Type)(f1 : B -> D)(f2 : C -> D)(ls1 : list B)(ls2 : list C)(a1 a2 : A), map (fun x => (a1, f1 x)) ls1 = map (fun x => (a2, f2 x)) ls2 -> ls1 <> nil -> a1 = a2.
proof: Proof. induction ls1; destruct ls2; intuition; simpl in *. discriminate. inversion H; clear H; subst. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation