proposition: Lemma sumList_f_inverse : forall (A B : Set)(ls : list A)(f : A -> B)(f_inv : B -> A)(fa : A -> Rat), (forall a, In a ls -> f_inv (f a) = a) -> sumList (map f ls) (fun (b : B) => fa (f_inv b) ) == sumList ls fa.
proof: Proof. intuition. unfold sumList. eapply fold_add_f_inverse; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia