proposition: Lemma fold_equiv_step : forall m f l a, Comm_monoid m -> noduplicates l -> mem a l -> exists l', fold m f l = fold m f (a::l') /\ (forall x, mem x l <-> mem x (a::l')) /\ noduplicates (a::l').
proof: Proof. Proof using. introv Hm. induction l as [|b t]; introv DL La. inverts La. tests: (a = b). exists t. splits*. inverts La. false. inverts DL as DLb DT. forwards~ (L'&EL'&EQ&DL'): IHt. exists (b::L'). splits. do 3 rewrite fold_cons. rewrite EL'. rewrite fold_cons. do 2 rewrite monoid_assoc. rewrite~ (monoid_comm (f b)). intros x. specializes EQ x. rewrite mem_cons_eq in EQ. do 3 rewrite mem_cons_eq. autos*. inverts DL'. constructors. introv N. inverts N. false. false. constructors~. introv N. applys DLb. rewrite EQ. constructors~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)