proposition: Theorem map_snd_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 (snd x)) (combine lsc ls).
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