proposition: Lemma fold_equiv : forall m f l1 l2, Comm_monoid m -> noduplicates l1 -> noduplicates l2 -> (forall x, mem x l1 <-> mem x l2) -> fold m f l1 = fold m f l2.
proof: Proof. Proof using. intros m f l1. induction l1; introv HM D1 D2 EQ. cuts_rewrite (l2 = nil). rewrite~ fold_nil. destruct l2; auto. forwards~ M: (proj2 (EQ a)). inverts M. inverts D1. asserts L2a: (mem a l2). rewrite~ <- EQ. forwards* (l2'&V2'&EQ'&D2'): fold_equiv_step f L2a. rewrite V2'. do 2 rewrite fold_cons. inverts D2'. rewrite~ (IHl1 l2'). intros. tests: (x = a). iff; auto_false*. asserts_rewrite (mem x l1 = mem x (a::l1)). extens. iff~ M. inverts~ M. false. asserts_rewrite (mem x l2' = mem x (a::l2')). extens. iff~ M. inverts~ M. false. rewrite EQ. rewrite* EQ'. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)