proposition: Theorem map_fst_eq : forall (C : Set)(lsc : list C)(A B : Set)(ls : list A)(f : A -> B), (length ls = length lsc) -> map f ls = map (fun x => f (fst x)) (combine ls lsc).
proof: Proof. induction lsc; destruct ls; intuition; simpl in *. lia. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation