diff --git a/LeanColls/Classes/IndexType/Basic.lean b/LeanColls/Classes/IndexType/Basic.lean
index eb41ff7ce..9e1702dc4 100644
--- a/LeanColls/Classes/IndexType/Basic.lean
+++ b/LeanColls/Classes/IndexType/Basic.lean
@@ -42,7 +42,8 @@ class IndexType.{u,w} (ι : Type u)
 
 class LawfulIndexType (ι : Type u) [I : IndexType ι]
   extends
-    Fold.ToList (IndexType.Univ ι) ι
+    Fold.LawfulFold (IndexType.Univ ι) ι,
+    Fold.AgreesWithToMultiset (IndexType.Univ ι) ι
   where
   leftInv  : Function.LeftInverse  I.fromFin I.toFin
   rightInv : Function.RightInverse I.fromFin I.toFin
@@ -113,11 +114,12 @@ instance (priority := default) : DecidableEq ι := by
 
 /-! #### Transport over equivalence -/
 
+
 def ofEquiv {ι} [IndexType.{_,w} ι'] (f : ι' ≃ ι) : IndexType.{_,w} ι where
   card := IndexType.card ι'
   toFin   := IndexType.toFin ∘ f.symm
   fromFin := f ∘ IndexType.fromFin
-  toFold := Fold.map (fun ⟨⟩ => IndexType.univ (ι')) f
+  toFold := Fold.instMap (fun ⟨⟩ => IndexType.univ (ι')) f
 
 def ofEquivLawful {ι} [I' : IndexType ι'] [LI' : LawfulIndexType ι'] (f : ι' ≃ ι)
     : @LawfulIndexType ι (ofEquiv f) :=
@@ -127,9 +129,17 @@ def ofEquivLawful {ι} [I' : IndexType ι'] [LI' : LawfulIndexType ι'] (f : ι'
     (leftInv  := by simp [ofEquiv]; intro; simp)
     (rightInv := by simp [ofEquiv]; intro; simp)
     (toList_eq_ofFn := by simp [ofEquiv]; rfl)
-    (toToList := by
-      letI := ofEquiv f; apply Fold.map.ToList
-      intro c'; simp [toList, ofEquiv, LawfulIndexType.toList_eq_ofFn]; rfl)
+    (toLawfulFold := Fold.LawfulFold.instMap ..)
+    (toAgreesWithToMultiset := by
+      convert @Fold.AgreesWithToMultiset.instMap _ _ _ _ _
+        inferInstance _ (fun (_ : Univ ι) => Univ.mk) f
+      simp [ofEquiv, inferInstance, ToMultiset.instMap]
+      unfold instToMultiset toMultiset
+      congr; ext _
+      have := LI'.toList_eq_ofFn
+      simp only [Multiset.map_coe, this]
+      congr; simp
+      rfl)
 
 /-! #### Unit -/
 
@@ -143,9 +153,9 @@ instance : IndexType Unit where
 instance : LawfulIndexType Unit where
   leftInv := by intro; rfl
   rightInv := by rintro ⟨i,h⟩; simp [card] at h; subst h; simp [fromFin, toFin]
-  fold_eq_fold_toList := by
+  exists_eq_list_foldl := by
     rintro ⟨⟩
-    refine ⟨_, .rfl, ?_⟩
+    refine ⟨_, rfl, ?_⟩
     intro β f init; simp [toList, fold]
   foldM_eq_fold := by
     rintro m β _ _ ⟨⟩ f init; simp [foldM, fold]
@@ -160,9 +170,9 @@ instance : IndexType (Fin n) where
 instance : LawfulIndexType (Fin n) where
   leftInv  := by intro _; rfl
   rightInv := by intro _; rfl
-  fold_eq_fold_toList := by
+  exists_eq_list_foldl := by
     rintro ⟨⟩
-    refine ⟨_, .rfl, ?_⟩
+    refine ⟨_, rfl, ?_⟩
     simp [toList, fold, Fin.foldl_eq_foldl_ofFn]
   foldM_eq_fold := by
     rintro β _ _ _ ⟨⟩ f init
@@ -179,10 +189,20 @@ instance : IndexType.{max u v, w} (α × β) where
   card := card α * card β
   toFin := fun (a,b) => Fin.pair (toFin a) (toFin b)
   fromFin := fun p => (fromFin (Fin.pair_left p), fromFin (Fin.pair_right p))
-  toList := fun ⟨⟩ => toList (univ α) ×ˢ toList (univ β)
-  toFold := @Fold.map (Univ α × Univ β) _ _ _
-    Fold.prod
-    (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+  toToList :=
+    let _ := ToList.instProd (C₁ := Univ α) (C₂ := Univ β)
+    ToList.instMap (C₁ := Univ α × Univ β) (C₂ := Univ (α × β)) (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+  toFold :=
+    let _ := Fold.instProd (C₁ := Univ α) (C₂ := Univ β)
+    Fold.instMap (C := Univ α × Univ β) (C' := Univ (α × β)) (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+
+@[simp]
+theorem toList_univ_prod {c : Univ (α × β)}: toList c = toList (univ α) ×ˢ toList (univ β) := by
+  simp [instIndexTypeProd, ToList.instMap, ToList.instProd]
+
+@[simp]
+theorem toMultiset_univ_prod : toMultiset (univ (α × β)) = toMultiset (univ α) ×ˢ toMultiset (univ β) := by
+  simp only [instIndexTypeProd, ToList.instMap, ToList.instProd, instToMultiset]; simp
 
 instance : LawfulIndexType.{max u v, w} (α × β) where
   rightInv := by
@@ -197,11 +217,33 @@ instance : LawfulIndexType.{max u v, w} (α × β) where
     simp [List.get_product_eq_get_pair]
     constructor <;>
       simp [← Fin.val_inj, Fin.pair_left, Fin.pair_right]
-  toToList :=
-    @Fold.map.ToList (Univ α × Univ β) _ _ _
-      (Fold.prod) (ToList.prod) (Fold.prod.ToList)
-      _ _ _
-      (by simp [toList, ToList.prod])
+  exists_eq_list_foldl :=
+    -- these proof goals are really annoying, and I'm not sure how to automate the
+    -- "just keep unfolding until we actually find the difference" step
+    let _a := Fold.instProd (C₁ := Univ α) (C₂ := Univ β)
+    let _b := Fold.instMap (C' := Univ (α × β)) (C := Univ α × Univ β)
+              (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+    let _c := ToMultiset.instProd (C₁ := Univ α) (C₂ := Univ β)
+    let _d := ToMultiset.instMap (C₂ := Univ (α × β)) (C₁ := Univ α × Univ β)
+              (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+    let _e := Fold.AgreesWithToMultiset.instProd (C₁ := Univ α) (C₂ := Univ β)
+    let f := Fold.AgreesWithToMultiset.instMap (C' := Univ (α × β)) (C := Univ α × Univ β)
+      (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+    by
+    have := f.exists_eq_list_foldl
+    intro c
+    specialize this c
+    rcases this with ⟨L,h1,h2⟩
+    refine ⟨L,?_,h2⟩
+    rw [h1]
+    simp (config := {zetaDelta := true})
+    simp only [ToMultiset.instMap, ToMultiset.instProd, toMultiset]
+    simp
+  toLawfulFold :=
+    @Fold.LawfulFold.instMap (Univ α × Univ β) _ (Univ (α × β)) _
+      Fold.instProd
+      Fold.LawfulFold.instProd
+      (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
 
 
 /-! #### Sigma -/
@@ -230,10 +272,26 @@ instance : IndexType.{max u v, w} (α ⊕ β) where
       .inl (fromFin ⟨i,h⟩)
     else
       .inr (fromFin ⟨i-card α, by simp at h; exact Nat.sub_lt_left_of_lt_add h hi⟩)
-  toList := fun ⟨⟩ => (toList (univ α)).map Sum.inl ++ (toList (univ β)).map Sum.inr
-  toFold := @Fold.map (Univ α × Univ β) _ _ _
-    Fold.sum
-    (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+  toToList :=
+    let _ := ToList.instSum (C₁ := Univ α) (C₂ := Univ β)
+    ToList.instMap (C₁ := Univ α × Univ β) (C₂ := Univ (α ⊕ β)) (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+  toFold :=
+    let _ := Fold.instSum (C₁ := Univ α) (C₂ := Univ β)
+    Fold.instMap (C := Univ α × Univ β) (C' := Univ (α ⊕ β)) (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+
+theorem toList_univ_sum {c : Univ (α ⊕ β)} :
+    toList c = (toList (univ α) |>.map Sum.inl) ++ (toList (univ β) |>.map Sum.inr) := by
+  simp [instIndexTypeSum, ToList.instMap, ToList.instSum]
+
+theorem toMultiset_univ_sum :
+    toMultiset (univ (α ⊕ β)) = (toMultiset (univ α)).map Sum.inl + (toMultiset (univ β)).map Sum.inr := by
+  simp only [instIndexTypeSum, ToList.instMap, ToList.instSum, instToMultiset]
+  simp only [
+    List.map_append,
+    List.map_map,
+    Function.id_comp,
+    ToList.toMultiset_toList]
+  rfl
 
 instance : LawfulIndexType (α ⊕ β) where
   leftInv := by
@@ -247,7 +305,7 @@ instance : LawfulIndexType (α ⊕ β) where
     else
       simp [*]; simp_all
   toList_eq_ofFn := by
-    simp [toList]
+    simp [toList_univ_sum, toList]
     apply List.ext_get
     · simp [card]
     intro i h1 h2
@@ -263,11 +321,30 @@ instance : LawfulIndexType (α ⊕ β) where
       · simpa using h
       · simp at h1 ⊢
         omega
-  toToList :=
-    @Fold.map.ToList (Univ α × Univ β) _ _ _
-      (Fold.sum) (ToList.sum) (Fold.sum.ToList)
-      _ _ _
-      (by simp [toList, ToList.sum])
+  exists_eq_list_foldl :=
+    -- these proof goals are really annoying, and I'm not sure how to automate the
+    -- "just keep unfolding until we actually find the difference" step
+    let _a := Fold.instSum (C₁ := Univ α) (C₂ := Univ β)
+    let _b := Fold.instMap (C' := Univ (α ⊕ β)) (C := Univ α × Univ β)
+              (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+    let _c := ToMultiset.instSum (C₁ := Univ α) (C₂ := Univ β)
+    let _d := ToMultiset.instMap (C₂ := Univ (α ⊕ β)) (C₁ := Univ α × Univ β)
+              (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+    let _e := Fold.AgreesWithToMultiset.instSum (C₁ := Univ α) (C₂ := Univ β)
+    let f := Fold.AgreesWithToMultiset.instMap (C' := Univ (α ⊕ β)) (C := Univ α × Univ β)
+      (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
+    by
+    have := f.exists_eq_list_foldl
+    intro c
+    specialize this c
+    rcases this with ⟨L,h1,h2⟩
+    refine ⟨L,?_,h2⟩
+    rw [h1]
+  toLawfulFold :=
+    @Fold.LawfulFold.instMap (Univ α × Univ β) _ (Univ (α ⊕ β)) _
+      Fold.instSum
+      Fold.LawfulFold.instSum
+      (fun ⟨⟩ => (⟨⟩,⟨⟩)) id
 
 
 end
diff --git a/LeanColls/Classes/Ops.lean b/LeanColls/Classes/Ops.lean
index 5b2e7b4cf..780965c26 100644
--- a/LeanColls/Classes/Ops.lean
+++ b/LeanColls/Classes/Ops.lean
@@ -4,6 +4,9 @@ Authors: James Gallicchio
 -/
 
 import LeanColls.MathlibUpstream
+import Mathlib.Data.Finset.Image
+import Mathlib.Data.Finset.Prod
+import Mathlib.Data.Finset.Sum
 
 /-! ## Collection operations
 
@@ -34,87 +37,202 @@ namespace LeanColls
 
 /-! ### Models -/
 
+/-- `C` can be modeled as a set of `τ`s -/
+class ToSet (C : Type u) (τ : outParam (Type v)) where
+  toSet : (cont : C) → Set τ
+export ToSet (toSet)
+
 /-- `C` can be modeled as a finset of `τ`s -/
 class ToFinset (C : Type u) (τ : outParam (Type v)) where
   toFinset : (cont : C) → Finset τ
+export ToFinset (toFinset)
 
 /-- `C` can be modeled as a multiset of `τ`s -/
 class ToMultiset (C : Type u) (τ : outParam (Type v)) where
   toMultiset : (cont : C) → Multiset τ
+export ToMultiset (toMultiset)
+
+/-- `C` can be modeled as a list of `τ`s -/
+class ToList (C : Type u) (τ : outParam (Type v)) where
+  toList : (cont : C) → List τ
+export ToList (toList)
+
+/-! #### Hierarchical Instances
 
-class LawfulToMultiset (C : Type u) (τ : outParam (Type v))
-        [DecidableEq τ] [ToFinset C τ] [ToMultiset C τ] where
-  toFinset_toMultiset : ∀ (cont : C),
-    (ToMultiset.toMultiset cont).toFinset = ToFinset.toFinset cont
+More specific models give a trivial default instance
+of the less specific model.
+-/
 
-attribute [simp] LawfulToMultiset.toFinset_toMultiset
+instance [ToFinset C τ] : ToSet C τ where
+  toSet c := toFinset c
 
 instance [DecidableEq τ] [ToMultiset C τ] : ToFinset C τ where
-  toFinset c := (ToMultiset.toMultiset c).toFinset
+  toFinset c := (toMultiset c).toFinset
 
-instance [DecidableEq τ] [ToMultiset C τ] : LawfulToMultiset C τ where
-  toFinset_toMultiset _ := rfl
+instance (priority := default + 1) [ToMultiset C τ] : ToSet C τ where
+  toSet c := (· ∈ toMultiset c)
 
-class ToList (C : Type u) (τ : outParam (Type v)) where
-  toList : (cont : C) → List τ
-export ToList (toList)
+instance [ToList C τ] : ToMultiset C τ where
+  toMultiset c := (toList c)
+
+/-! #### Lemmas -/
+
+namespace ToSet
+
+@[inline]
+def instProd [ToSet C₁ τ₁] [ToSet C₂ τ₂] : ToSet (C₁ × C₂) (τ₁ × τ₂) where
+  toSet := fun (c1,c2) => toSet c1 ×ˢ toSet c2
+
+@[inline]
+def instSum [ToSet C₁ τ₁] [ToSet C₂ τ₂] : ToSet (C₁ × C₂) (τ₁ ⊕ τ₂) where
+  toSet := fun (c1,c2) =>
+    ((toSet c1).image Sum.inl) ∪ ((toSet c2).image Sum.inr)
+
+@[inline]
+def instMap [ToSet C₁ τ₁] (fC : C₂ → C₁) (ft : τ₁ → τ₂) : ToSet C₂ τ₂ where
+  toSet c2 := toSet (fC c2) |>.image ft
+
+end ToSet
+
+namespace ToFinset
+
+@[simp]
+theorem toSet_toFinset [ToFinset C τ] (c : C) : (toFinset c).toSet = toSet c := rfl
+
+@[inline]
+def instProd [ToFinset C₁ τ₁] [ToFinset C₂ τ₂] : ToFinset (C₁ × C₂) (τ₁ × τ₂) where
+  toFinset := fun (c1,c2) => toFinset c1 ×ˢ toFinset c2
+
+@[inline]
+def instSum [ToFinset C₁ τ₁] [ToFinset C₂ τ₂] : ToFinset (C₁ × C₂) (τ₁ ⊕ τ₂) where
+  toFinset := fun (c1,c2) =>
+    Finset.disjSum (toFinset c1) (toFinset c2)
+
+@[inline]
+def instMap [ToFinset C₁ τ₁] (fC : C₂ → C₁) (ft : τ₁ ↪ τ₂) : ToFinset C₂ τ₂ where
+  toFinset c2 := toFinset (fC c2) |>.map ft
 
-class LawfulToList (C : Type u) (τ : outParam (Type v))
-        [ToMultiset C τ] [ToList C τ] where
-  toMultiset_toList : ∀ (cont : C), (toList cont) = ToMultiset.toMultiset cont
+end ToFinset
 
-attribute [simp] LawfulToMultiset.toFinset_toMultiset
+namespace ToMultiset
+
+@[simp]
+theorem toFinset_toMultiset [DecidableEq τ] [ToMultiset C τ] (c : C)
+  : (toMultiset c).toFinset = toFinset c := rfl
+
+@[inline]
+def instProd [ToMultiset C₁ τ₁] [ToMultiset C₂ τ₂] : ToMultiset (C₁ × C₂) (τ₁ × τ₂) where
+  toMultiset := fun (c1,c2) => toMultiset c1 ×ˢ toMultiset c2
+
+@[inline]
+def instSum [ToMultiset C₁ τ₁] [ToMultiset C₂ τ₂] : ToMultiset (C₁ × C₂) (τ₁ ⊕ τ₂) where
+  toMultiset := fun (c1,c2) =>
+    (toMultiset c1).map Sum.inl + (toMultiset c2).map Sum.inr
+
+@[inline]
+def instMap [ToMultiset C₁ τ₁] (fC : C₂ → C₁) (ft : τ₁ → τ₂) : ToMultiset C₂ τ₂ where
+  toMultiset c2 := toMultiset (fC c2) |>.map ft
+
+end ToMultiset
 
 namespace ToList
 
-instance [ToList C τ] : ToMultiset C τ where
-  toMultiset c := (toList c)
+@[simp]
+theorem toMultiset_toList [ToList C τ] (c : C)
+  : Multiset.ofList (toList c) = toMultiset c := rfl
 
-instance [ToList C τ] : LawfulToList C τ where
-  toMultiset_toList _ := rfl
+@[simp]
+theorem toFinset_toList [ToList C τ] [DecidableEq τ] (c : C)
+  : (toList c).toFinset = toFinset c := rfl
 
-def prod [ToList C₁ τ₁] [ToList C₂ τ₂] : ToList (C₁ × C₂) (τ₁ × τ₂) where
+@[inline]
+def instProd [ToList C₁ τ₁] [ToList C₂ τ₂] : ToList (C₁ × C₂) (τ₁ × τ₂) where
   toList := fun (c1,c2) => toList c1 ×ˢ toList c2
 
-def sum [ToList C₁ τ₁] [ToList C₂ τ₂] : ToList (C₁ × C₂) (τ₁ ⊕ τ₂) where
+@[simp]
+theorem instProd.toToMultiset_eq_toMultiset_prod [ToList C₁ τ₁] [ToList C₂ τ₂] (c1 : C₁) (c2 : C₂)
+  : ↑(toList c1 ×ˢ toList c2) = toMultiset c1 ×ˢ toMultiset c2 := by
+  simp only [instToMultiset]
+  rw [Multiset.coe_product]
+
+@[inline]
+def instSum [ToList C₁ τ₁] [ToList C₂ τ₂] : ToList (C₁ × C₂) (τ₁ ⊕ τ₂) where
   toList := fun (c1,c2) =>
     (toList c1).map Sum.inl ++ (toList c2).map Sum.inr
 
+@[inline]
+def instMap [ToList C₁ τ₁] (fC : C₂ → C₁) (ft : τ₁ → τ₂) : ToList C₂ τ₂ where
+  toList c2 := toList (fC c2) |>.map ft
+
 end ToList
 
 
 /-! ### Operations Defined Elsewhere -/
 
-namespace Mem
-variable (C : Type u) (τ : outParam (Type v)) [Membership τ C]
+namespace Membership
+
+/-- Correctness of `Membership` against the `ToSet` model. -/
+class AgreesWithToSet (C : Type u) (τ : outParam (Type v)) [Membership τ C] [ToSet C τ] : Prop where
+  mem_iff_mem_toSet : ∀ x (cont : C), x ∈ cont ↔ x ∈ toSet cont
+export AgreesWithToSet (mem_iff_mem_toSet)
+
+variable {C τ} [Membership τ C]
 
-class ToFinset [ToFinset C τ] : Prop where
-  mem_iff_mem_toFinset : ∀ x (cont : C),
-    x ∈ cont ↔ x ∈ ToFinset.toFinset cont
+/-!
+Simp normal form for membership is `x ∈ c` with the smallest expression `c`.
+-/
+
+@[simp] theorem mem_toSet_iff_mem (c : C) [ToSet C τ] [AgreesWithToSet C τ]
+  : x ∈ toSet c ↔ x ∈ c := by
+  simp [mem_iff_mem_toSet]
+
+@[simp] theorem mem_toFinset_iff_mem (c : C) [ToFinset C τ] [AgreesWithToSet C τ]
+  : x ∈ toFinset c ↔ x ∈ c := by
+  simp [← Finset.mem_coe]
 
-class ToMultiset [ToMultiset C τ] : Prop where
-  mem_iff_mem_toMultiset : ∀ x (cont : C),
-    x ∈ cont ↔ x ∈ ToMultiset.toMultiset cont
+@[simp] theorem mem_toMultiset_iff_mem (c : C) [ToMultiset C τ] [AgreesWithToSet C τ]
+  : x ∈ toMultiset c ↔ x ∈ c := by
+  simp [mem_iff_mem_toSet, instToSet_1]
+  rfl
 
-class ToList [ToList C τ] : Prop where
-  mem_iff_mem_toList : ∀ x (cont : C),
-    x ∈ cont ↔ x ∈ ToList.toList cont
+@[simp] theorem mem_toList_iff_mem (c : C) [ToList C τ] [AgreesWithToSet C τ]
+  : x ∈ toList c ↔ x ∈ c := by
+  conv => rhs; rw [mem_iff_mem_toSet]
+
+/-! Different simp normal form would be to reduce membership to membership
+in the base model for the collection.
+
+TODO: how to handle this?
+-/
 
-end Mem
+theorem mem_toSet_iff_mem_toFinset [ToFinset C τ] (x : τ) (c : C) :
+    x ∈ toSet c ↔ x ∈ toFinset c := by rfl
+
+theorem mem_toSet_iff_mem_toMultiset [ToMultiset C τ] (x : τ) (c : C) :
+    x ∈ toSet c ↔ x ∈ toMultiset c := by rfl
+
+theorem mem_toFinset_iff_mem_toMultiset [ToMultiset C τ] [DecidableEq τ] (x : τ) (c : C) :
+    x ∈ toFinset c ↔ x ∈ toMultiset c := by
+  simp only [instToFinset, Multiset.mem_toFinset]
+
+theorem mem_toMultiset_iff_mem_toList [ToList C τ] (x : τ) (c : C) :
+    x ∈ toMultiset c ↔ x ∈ toList c := by
+  simp only [instToMultiset]; rw [Multiset.mem_coe]
+
+end Membership
 
 namespace Append
 variable (C : Type u) (τ : outParam (Type v)) [Append C]
 
-class ToList [ToList C τ] : Prop where
+class AgreesWithToList [ToList C τ] : Prop where
   toList_append : ∀ (c1 c2 : C),
     toList (c1 ++ c2) = toList c1 ++ toList c2
+export AgreesWithToList (toList_append)
 
-attribute [simp] ToList.toList_append
+attribute [simp] toList_append
 
 end Append
 
-export Functor (map)
-
 namespace Functor
 variable (C : Type u → Type v) [Functor C] (τ τ')
 
diff --git a/LeanColls/Classes/Ops/Fold.lean b/LeanColls/Classes/Ops/Fold.lean
index 7c3b6b47d..eba2aab7a 100644
--- a/LeanColls/Classes/Ops/Fold.lean
+++ b/LeanColls/Classes/Ops/Fold.lean
@@ -6,34 +6,52 @@ Authors: James Gallicchio
 import LeanColls.MathlibUpstream
 import LeanColls.Classes.Ops
 
+import Mathlib.Data.Finset.Basic
+
 namespace LeanColls.Fold
 
-variable [Fold C τ] [LeanColls.ToList C τ]
+variable [Fold C τ]
+
+/-- States that `foldM` is equivalent to `fold`. -/
+class LawfulFold (C τ) [Fold C τ] : Prop where
+  /-- `foldM` is equivalent to doing a fold and binding on each intermediary.
 
-/-- Correctness of `Fold` with respect to `ToList` -/
-class ToList (C τ) [Fold C τ] [ToList C τ] : Prop where
-  fold_eq_fold_toList : ∀ (c : C), ∃ L,
-      List.Perm L (toList c) ∧
-      ∀ {β} (f) (init : β), fold c f init = List.foldl f init L
+  This is generally not definitionally true.
+  Most `foldM` implementations can "early exit" the fold by
+  putting the next iteration/recursive call within the continuation to bind. -/
   foldM_eq_fold : [Monad m] → [LawfulMonad m] → ∀ (c : C) (f) (init : β),
     foldM (m := m) c f init = fold c (fun acc x => acc >>= (f · x)) (pure init)
+export LawfulFold (foldM_eq_fold)
 
-variable [ToList C τ]
+/-- Correctness of `Fold` with respect to `ToMultiset` -/
+class AgreesWithToMultiset (C τ) [Fold C τ] [ToMultiset C τ] : Prop where
+  /-- `fold` on `c` corresponds to a `List.foldl` on some list with all the elements in `c`.
+    We only require `ToMultiset` because the fold already can occur in any order.
 
-theorem foldM_eq_foldM_toList [Monad m] [LawfulMonad m] (c : C)
-  : ∃ L, List.Perm L (toList c) ∧
-    ∀ {β} (f) (init : β), foldM (m := m) c f init = List.foldlM f init L
+    Note: the list is determined wholly by `c : C`,
+    to ensure the order of elements being folded is consistent
+    regardless of the fold function/accumulator. -/
+  exists_eq_list_foldl : ∀ (c : C),
+    ∃ L : List τ, L = toMultiset c ∧
+    ∀ {β} (f) (init : β), fold c f init = List.foldl f init L
+export AgreesWithToMultiset (exists_eq_list_foldl)
+
+section
+variable [ToMultiset C τ] [AgreesWithToMultiset C τ]
+
+theorem exists_eq_list_foldr (c : C)
+  : ∃ L : List τ, L = toMultiset c ∧
+    ∀ {β} (f) (init : β), fold c f init = List.foldr (Function.swap f) init L
   := by
-  have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
-  use L; refine ⟨perm,?_⟩; clear perm
-  intro β f init
-  rw [ToList.foldM_eq_fold, h, List.foldlM_eq_foldl]
+  have ⟨L,hL,h⟩ := exists_eq_list_foldl c
+  use L.reverse
+  simp [hL, h]
 
 /-- A strange lemma. Analogous to `bind_pure` chained over the length of `c`. -/
-theorem bind_fold_pure [ToList C τ] [Monad m] [LawfulMonad m] (ma : m α) (c : C) (f : _ → _ → _)
+theorem bind_fold_pure [Monad m] [LawfulMonad m] (ma : m α) (c : C) (f : _ → _ → _)
   : ma >>= (fun a => fold c (fun acc t => do let acc ← acc; f acc t) (pure a)) =
     fold c (fun acc t => do let acc ← acc; f acc t) ma := by
-  have := ToList.fold_eq_fold_toList c
+  have := exists_eq_list_foldl c
   rcases this with ⟨L,-,h⟩
   simp [h]; clear h
   rw [← List.foldr_reverse]
@@ -45,31 +63,123 @@ theorem bind_fold_pure [ToList C τ] [Monad m] [LawfulMonad m] (ma : m α) (c :
     simp; rw [← ih]
     simp
 
+theorem multisetInduction
+    (c : C) {f acc} {motive : Multiset τ → β → Prop}
+    (empty : motive ∅ acc)
+    (cons : ∀ {m acc x}, m ⊆ toMultiset c → x ∈ toMultiset c → motive m acc → motive (x ::ₘ m) (f acc x))
+  : motive (toMultiset c) (fold c f acc) := by
+  have ⟨L,hL,h⟩ := exists_eq_list_foldr c
+  rw [h]; clear h
+  rw [← hL]
+  have : ∀ x ∈ L, x ∈ toMultiset c := by
+    intro x hx; rw [← Multiset.mem_coe, hL] at hx
+    simpa [Membership.mem_iff_mem_toSet] using hx
+  clear hL
+  induction L with
+  | nil =>
+    simp; exact empty
+  | cons hd tl ih =>
+    simp [Function.swap]; rw [← Multiset.cons_coe]
+    apply cons
+    · aesop
+    · aesop
+    · apply ih
+      aesop
+
+variable [LawfulFold C τ]
+
+theorem exists_eq_list_foldlM [Monad m] [LawfulMonad m] (c : C)
+  : ∃ L : List τ, L = toMultiset c ∧
+    ∀ {β} (f) (init : β), foldM (m := m) c f init = List.foldlM f init L
+  := by
+  have ⟨L,hL,h⟩ := exists_eq_list_foldl c
+  use L; refine ⟨hL,?_⟩; clear hL
+  intro β f init
+  rw [foldM_eq_fold, h, List.foldlM_eq_foldl]
+
+theorem exists_eq_list_foldrM [Monad m] [LawfulMonad m] (c : C)
+  : ∃ L : List τ, L = toMultiset c ∧
+    ∀ {β} (f) (init : β), foldM (m := m) c f init = List.foldrM (Function.swap f) init L
+  := by
+  have ⟨L,hL,h⟩ := exists_eq_list_foldr c
+  use L; refine ⟨hL,?_⟩; clear hL
+  intro β f init
+  rw [foldM_eq_fold, h, List.foldrM_eq_foldr]
+
+end
+
+
+/-! #### Directed Folds -/
+
+def AgreesWithToMultiset.instOfFoldr [ToMultiset C τ] (h : ∀ (c : C),
+    ∃ L : List τ, L = toMultiset c ∧
+    ∀ {β} (f) (init : β), fold c f init = List.foldr (Function.swap f) init L)
+  : AgreesWithToMultiset C τ where
+  exists_eq_list_foldl c := by
+    have := h c; clear h
+    rcases this with ⟨L,h⟩
+    use L.reverse
+    simp [h]
+
+/-- Types `C` for which `fold` on `c : C` is the same as `foldl` on `toList c`. -/
+class AgreesWithToList.Foldl (C τ) [Fold C τ] [ToList C τ] : Prop where
+  /-- `fold c` is the same as `List.foldl` over `toList c` -/
+  fold_eq_foldl_toList : ∀ (c : C) {β} (f) (init : β),
+    fold c f init = List.foldl f init (toList c)
+export AgreesWithToList.Foldl (fold_eq_foldl_toList)
+
+instance [ToList C τ] [AgreesWithToList.Foldl C τ] : AgreesWithToMultiset C τ where
+  exists_eq_list_foldl c := by
+    use toList c
+    constructor
+    · simp
+    · apply fold_eq_foldl_toList
+
+/-- Types `C` for which `fold` on `c : C` is the same as `foldr` on `toList c`. -/
+class AgreesWithToList.Foldr (C τ) [Fold C τ] [ToList C τ] : Prop where
+  /-- `fold c` is the same as `List.foldr` over `toList c` -/
+  fold_eq_foldr_toList : ∀ (c : C) {β} (f) (init : β),
+    fold c f init = List.foldr (Function.swap f) init (toList c)
+export AgreesWithToList.Foldr (fold_eq_foldr_toList)
+
+instance [ToList C τ] [AgreesWithToList.Foldr C τ] : AgreesWithToMultiset C τ where
+  exists_eq_list_foldl c := by
+    use (toList c).reverse
+    simp
+    apply fold_eq_foldr_toList
+
+/-! #### Constructing Fold instances -/
+
 @[inline]
-def map [Fold C τ] (fc : C' → C) (ft : τ → τ') : Fold C' τ' where
+def instMap [Fold C τ] (fc : C' → C) (ft : τ → τ') : Fold C' τ' where
   fold  c h init := Fold.fold  (fc c) (fun acc x => h acc (ft x)) init
   foldM c h init := Fold.foldM (fc c) (fun acc x => h acc (ft x)) init
 
-def map.ToList [F : Fold C τ] [LeanColls.ToList C τ] [ToList C τ]
-              [L : LeanColls.ToList C' τ'] (fc : C' → C) (ft : τ → τ')
-              (h : ∀ c', toList c' = List.map ft (toList (fc c')))
-    : @ToList C' τ' (map fc ft) L :=
-  @ToList.mk _ _ (map fc ft) L
+nonrec def LawfulFold.instMap [F : Fold C τ] [LF : LawfulFold C τ] (fc : C' → C) (ft : τ → τ')
+    : @LawfulFold C' τ' (instMap fc ft) :=
+  @LawfulFold.mk _ _ (instMap fc ft)
     (by
+      intro m β M LM c' g init
+      simp [instMap, foldM_eq_fold])
+
+nonrec def AgreesWithToMultiset.instMap [Fold C τ] [ToMultiset C τ] [AgreesWithToMultiset C τ]
+        (fc : C' → C) (ft : τ → τ')
+    : @AgreesWithToMultiset C' τ' (instMap fc ft) (ToMultiset.instMap fc ft) :=
+  @AgreesWithToMultiset.mk _ _ (instMap fc ft) (ToMultiset.instMap fc ft)
+      (by
       intro c'
-      have ⟨L,hL,hfold⟩ := ToList.fold_eq_fold_toList (fc c')
+      have ⟨L,hL,hfold⟩ := AgreesWithToMultiset.exists_eq_list_foldl (fc c')
       use L.map ft
       constructor
-      · rw [h]; apply List.Perm.map; apply hL
-      intro β g init
-      specialize hfold (fun acc x => g acc (ft x)) init
-      simp [map, hfold, List.foldl_map])
-    (by
-      intro m β M LM c' g init
-      simp [map, ToList.foldM_eq_fold])
+      · rw [← Multiset.map_coe, hL]; simp [ToMultiset.instMap]
+      · intro β g init
+        specialize hfold (fun acc x => g acc (ft x)) init
+        simp [instMap, hfold, List.foldl_map])
+
+
 
 @[inline]
-def prod [Fold C₁ τ₁] [Fold C₂ τ₂] : Fold (C₁ × C₂) (τ₁ × τ₂) where
+def instProd [Fold C₁ τ₁] [Fold C₂ τ₂] : Fold (C₁ × C₂) (τ₁ × τ₂) where
   fold := fun (c1,c2) f init =>
     init |> fold c1 fun acc x1 =>
       acc |> fold c2 fun acc x2 => f acc (x1,x2)
@@ -77,30 +187,37 @@ def prod [Fold C₁ τ₁] [Fold C₂ τ₂] : Fold (C₁ × C₂) (τ₁ × τ
     init |> foldM c1 fun acc x1 =>
       acc |> foldM c2 fun acc x2 => f acc (x1,x2)
 
-def prod.ToList [Fold C₁ τ₁] [L₁ : LeanColls.ToList C₁ τ₁] [Fold.ToList C₁ τ₁]
-                [Fold C₂ τ₂] [L₂ : LeanColls.ToList C₂ τ₂] [Fold.ToList C₂ τ₂]
-  : @ToList (C₁ × C₂) (τ₁ × τ₂) prod .prod :=
-  @ToList.mk _ _ prod .prod
+nonrec def LawfulFold.instProd [Fold C₁ τ₁] [LawfulFold C₁ τ₁] [Fold C₂ τ₂] [LawfulFold C₂ τ₂]
+    [ToMultiset C₂ τ₂] [AgreesWithToMultiset C₂ τ₂]
+  : @LawfulFold (C₁ × C₂) (τ₁ × τ₂) instProd :=
+  @LawfulFold.mk (C₁ × C₂) (τ₁ × τ₂) instProd
+    (by
+    rintro m β M LM ⟨c1,c2⟩ f acc
+    simp [instProd]
+    rw [LawfulFold.foldM_eq_fold]
+    congr; funext acc x
+    conv => lhs; rhs; ext; rw [LawfulFold.foldM_eq_fold]
+    rw [bind_fold_pure]
+    )
+
+nonrec def AgreesWithToMultiset.instProd
+    [Fold C₁ τ₁] [ToMultiset C₁ τ₁] [AgreesWithToMultiset C₁ τ₁]
+    [Fold C₂ τ₂] [ToMultiset C₂ τ₂] [AgreesWithToMultiset C₂ τ₂]
+  : @AgreesWithToMultiset (C₁ × C₂) (τ₁ × τ₂) instProd .instProd :=
+  @AgreesWithToMultiset.mk _ _ instProd .instProd
   (by
     rintro ⟨c1,c2⟩
-    have ⟨L1,hL1,h1⟩ := Fold.ToList.fold_eq_fold_toList c1
-    have ⟨L2,hL2,h2⟩ := Fold.ToList.fold_eq_fold_toList c2
+    have ⟨L1,hL1,h1⟩ := AgreesWithToMultiset.exists_eq_list_foldl c1
+    have ⟨L2,hL2,h2⟩ := AgreesWithToMultiset.exists_eq_list_foldl c2
     use L1 ×ˢ L2
     constructor
-    · simp [ToList.prod]; apply List.Perm.product hL1 hL2
-    intro β f init
-    simp [prod, ToList.prod]
-    simp_rw [h1, h2, List.foldl_product])
-  (by
-    rintro m γ _ _ ⟨c1,c2⟩ f init
-    simp [prod, ToList.foldM_eq_fold]
-    congr
-    funext acc x
-    rw [bind_fold_pure]
-  )
+    · simp [ToMultiset.instProd]; rw [← Multiset.coe_product, hL1, hL2]
+    · intro β f init
+      simp [instProd, ToMultiset.instProd]
+      simp_rw [h1, h2, List.foldl_product])
 
 @[inline]
-def sum [Fold C₁ τ₁] [Fold C₂ τ₂] : Fold (C₁ × C₂) (τ₁ ⊕ τ₂) where
+def instSum [Fold C₁ τ₁] [Fold C₂ τ₂] : Fold (C₁ × C₂) (τ₁ ⊕ τ₂) where
   fold := fun (c1,c2) f init =>
     init
     |> fold c1 (fun acc x => f acc (.inl x))
@@ -109,27 +226,35 @@ def sum [Fold C₁ τ₁] [Fold C₂ τ₂] : Fold (C₁ × C₂) (τ₁ ⊕ τ
     let acc ← foldM c1 (fun acc x => f acc (.inl x)) acc
     foldM c2 (fun acc x => f acc (.inr x)) acc
 
-def sum.ToList [Fold C₁ τ₁] [L₁ : LeanColls.ToList C₁ τ₁] [Fold.ToList C₁ τ₁]
-                [Fold C₂ τ₂] [L₂ : LeanColls.ToList C₂ τ₂] [Fold.ToList C₂ τ₂]
-  : @ToList (C₁ × C₂) (τ₁ ⊕ τ₂) sum .sum :=
-  @ToList.mk _ _ sum .sum
-  (by
-    rintro ⟨c1,c2⟩
-    have ⟨L1,hL1,h1⟩ := Fold.ToList.fold_eq_fold_toList c1
-    have ⟨L2,hL2,h2⟩ := Fold.ToList.fold_eq_fold_toList c2
-    simp [ToList.sum, sum]
-    use L1.map Sum.inl ++ L2.map Sum.inr
-    constructor
-    · apply List.Perm.append <;> (apply List.Perm.map; assumption)
-    intro β f init
-    rw [h1, h2]
-    simp [List.foldl_map])
+nonrec def LawfulFold.instSum
+    [Fold C₁ τ₁] [LawfulFold C₁ τ₁]
+    [Fold C₂ τ₂] [LawfulFold C₂ τ₂]
+    [ToMultiset C₂ τ₂] [AgreesWithToMultiset C₂ τ₂]
+  : @LawfulFold (C₁ × C₂) (τ₁ ⊕ τ₂) instSum :=
+  @LawfulFold.mk _ _ instSum
   (by
     rintro m γ _ _ ⟨c1,c2⟩ f init
-    simp [sum, ToList.foldM_eq_fold]
+    simp [instSum, LawfulFold.foldM_eq_fold]
     rw [bind_fold_pure]
   )
 
+nonrec def AgreesWithToMultiset.instSum
+    [Fold C₁ τ₁] [ToMultiset C₁ τ₁] [AgreesWithToMultiset C₁ τ₁]
+    [Fold C₂ τ₂] [ToMultiset C₂ τ₂] [AgreesWithToMultiset C₂ τ₂]
+  : @AgreesWithToMultiset (C₁ × C₂) (τ₁ ⊕ τ₂) instSum .instSum :=
+  @AgreesWithToMultiset.mk _ _ instSum .instSum
+  (by
+    rintro ⟨c1,c2⟩
+    have ⟨L1,hL1,h1⟩ := AgreesWithToMultiset.exists_eq_list_foldl c1
+    have ⟨L2,hL2,h2⟩ := AgreesWithToMultiset.exists_eq_list_foldl c2
+    simp [instSum, ToMultiset.instSum]
+    use L1.map Sum.inl ++ L2.map Sum.inr
+    constructor
+    · rw [← hL1, ← hL2]; simp
+    · intro β f init
+      rw [h1, h2]
+      simp [List.foldl_map])
+
 instance : ForIn m C τ where
   forIn := fun {β} _ c acc f => do
     let res ← Fold.foldM (m := ExceptT β m)
@@ -168,72 +293,72 @@ def all (f : τ → Bool) (cont : C) : Bool :=
   | Except.ok () => true
   | Except.error () => false
 
-theorem any_eq_any_toList [LeanColls.ToList C τ] [ToList C τ]
+theorem any_iff_exists_toMultiset [LawfulFold C τ]
+    [ToMultiset C τ] [AgreesWithToMultiset C τ]
     (f : τ → Bool) (c : C)
-  : any f c = List.any (toList c) f := by
+  : any f c ↔ (∃ x ∈ toMultiset c, f x) := by
   unfold any
   generalize hf' : (fun _ _ => _) = f'
-  suffices foldM c f' () = Except.error () ↔ List.any (toList c) f by
+  suffices foldM c f' () = Except.error () ↔ ∃ x ∈ toMultiset c, f x by
     rw [eq_comm]; split
     · rw [Bool.eq_false_iff]; aesop
     · aesop
-  rw [ToList.foldM_eq_fold]
-  have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
-  rw [h]; clear h
-  simp_rw [List.any_eq_true, ← perm.mem_iff]; clear perm c
-  subst hf'
-  rw [← List.foldlM_eq_foldl]
-  induction L with
-  | nil => simp_all [pure, Except.pure]
-  | cons hd tl ih =>
-    simp [bind, Except.bind]
-    by_cases f hd = true <;> simp_all
+  rw [foldM_eq_fold]
+  apply multisetInduction (motive := fun m acc => acc = Except.error () ↔ ∃ x ∈ m, f x)
+  · simp [pure, Except.pure]
+  · intro m acc x _ _ ih
+    simp; rw [← ih]; clear ih
+    cases acc
+    case error =>
+      simp [hf'.symm, bind, Except.bind]
+    case ok =>
+      simp [hf'.symm, bind, Except.bind]
 
-theorem all_eq_all_toList [LeanColls.ToList C τ] [ToList C τ]
+theorem all_iff_exists_toMultiset [LawfulFold C τ]
+    [ToMultiset C τ] [AgreesWithToMultiset C τ]
     (f : τ → Bool) (c : C)
-  : all f c = List.all (toList c) f := by
+  : all f c ↔ (∀ x ∈ toMultiset c, f x) := by
   unfold all
   generalize hf' : (fun _ _ => _) = f'
-  suffices foldM c f' () = Except.ok () ↔ List.all (toList c) f by
-    rw [eq_comm]; split
-    · aesop
-    · rw [Bool.eq_false_iff]; aesop
-  rw [ToList.foldM_eq_fold]
-  have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
-  rw [h]; clear h
-  simp_rw [List.all_eq_true, ← perm.mem_iff]; clear perm c
-  subst hf'
-  rw [← List.foldlM_eq_foldl]
-  induction L with
-  | nil => simp_all [pure, Except.pure]
-  | cons hd tl ih =>
-    simp [bind, Except.bind]
-    by_cases f hd = true <;> simp_all
+  suffices foldM c f' () = Except.ok () ↔ ∀ x ∈ toMultiset c, f x by
+    rw [eq_comm]; split <;> aesop
+  rw [foldM_eq_fold]
+  apply multisetInduction (motive := fun m acc => acc = Except.ok () ↔ ∀ x ∈ m, f x)
+  · simp [pure, Except.pure]
+  · intro m acc x _ _ ih
+    simp; rw [← ih]; clear ih
+    cases acc
+    case error =>
+      simp [hf'.symm, bind, Except.bind]
+    case ok =>
+      simp [hf'.symm, bind, Except.bind]
 
 @[simp]
-theorem any_iff_exists [Membership τ C] [LeanColls.ToList C τ] [ToList C τ] [Mem.ToList C τ]
+theorem any_iff_exists [LawfulFold C τ] [Membership τ C]
+    [ToMultiset C τ] [AgreesWithToMultiset C τ] [Membership.AgreesWithToSet C τ]
     (f : τ → Bool) (c : C)
   : any f c ↔ ∃ x ∈ c, f x := by
-  rw [any_eq_any_toList]
-  simp [Mem.ToList.mem_iff_mem_toList]
+  rw [any_iff_exists_toMultiset]; simp
 
 @[simp]
-theorem all_iff_exists [Membership τ C] [LeanColls.ToList C τ] [ToList C τ] [Mem.ToList C τ]
+theorem all_iff_exists [LawfulFold C τ] [Membership τ C]
+    [ToMultiset C τ] [AgreesWithToMultiset C τ] [Membership.AgreesWithToSet C τ]
     (f : τ → Bool) (c : C)
   : all f c ↔ ∀ x ∈ c, f x := by
-  rw [all_eq_all_toList]
-  simp [Mem.ToList.mem_iff_mem_toList]
+  rw [all_iff_exists_toMultiset]; simp
 
-def toMem [Fold C τ] : Membership τ C where
+def instMem : Membership τ C where
   mem x c := open Classical in any (decide <| · = x) c
 
-def toMem.ToList [Fold C τ] [LeanColls.ToList C τ] [ToList C τ]
-    : @Mem.ToList C τ toMem inferInstance :=
-  @Mem.ToList.mk C τ toMem inferInstance
+def instMem.AgreesWithToSet [DecidableEq τ] [LawfulFold C τ]
+      [ToMultiset C τ] [AgreesWithToMultiset C τ]
+  : @Membership.AgreesWithToSet C τ instMem inferInstance :=
+  @Membership.AgreesWithToSet.mk C τ instMem inferInstance
     (by
       intro x c
-      simp [toMem]
-      rw [any_eq_any_toList]
-      simp [List.any_eq_true, beq_iff_eq, exists_eq_right])
+      simp [instMem]
+      rw [any_iff_exists_toMultiset]
+      simp [List.any_eq_true, beq_iff_eq, exists_eq_right]
+      rfl)
 
 end Fold
diff --git a/LeanColls/Classes/Ops/Insert.lean b/LeanColls/Classes/Ops/Insert.lean
index fa61b73fa..ace783368 100644
--- a/LeanColls/Classes/Ops/Insert.lean
+++ b/LeanColls/Classes/Ops/Insert.lean
@@ -14,41 +14,52 @@ instance [_root_.Insert τ C] [EmptyCollection C] : Insert C τ where
 
 variable  (C : Type u) (τ : outParam (Type v)) [Insert C τ]
 
-class Mem [Membership τ C] : Prop where
-  mem_empty : ∀ x, ¬ x ∈ empty (C := C)
-  mem_insert : ∀ x (cont : C) y, x ∈ insert cont y ↔ x = y ∨ x ∈ cont
-  mem_singleton : ∀ x y, x ∈ singleton (C := C) y ↔ x = y
+class AgreesWithToSet [ToSet C τ] : Prop where
+  toSet_empty : toSet (empty (C := C)) = ∅
+  toSet_insert : ∀ (cont : C) x, toSet (insert cont x) = {x} ∪ toSet cont
+  toSet_singleton : ∀ x, toSet (singleton (C := C) x) = {x}
 
-class ToMultiset [ToMultiset C τ] : Prop where
-  toMultiset_empty : ToMultiset.toMultiset (empty (C := C)) = {}
+export AgreesWithToSet (
+  toSet_empty
+  toSet_insert
+  toSet_singleton)
+
+attribute [simp] toSet_empty toSet_insert toSet_singleton
+
+class AgreesWithToMultiset [ToMultiset C τ] : Prop where
+  toMultiset_empty : toMultiset (empty (C := C)) = 0
   toMultiset_insert : ∀ (cont : C) x,
-    ToMultiset.toMultiset (insert cont x) = Multiset.cons x (ToMultiset.toMultiset cont)
+    toMultiset (insert cont x) = x ::ₘ toMultiset cont
   toMultiset_singleton : ∀ x,
-    ToMultiset.toMultiset (singleton (C := C) x) = {x}
+    toMultiset (singleton (C := C) x) = {x}
 
-instance [Membership τ C] [LeanColls.ToMultiset C τ] [ToMultiset C τ] [Mem.ToMultiset C τ] : Mem C τ where
-  mem_empty := by
-    intro x
-    simp [Mem.ToMultiset.mem_iff_mem_toMultiset, ToMultiset.toMultiset_empty]
-  mem_insert := by
-    intro x c y
-    simp [Mem.ToMultiset.mem_iff_mem_toMultiset, ToMultiset.toMultiset_insert]
-  mem_singleton := by
+export AgreesWithToMultiset (
+  toMultiset_empty
+  toMultiset_insert
+  toMultiset_singleton)
+
+attribute [simp] toMultiset_empty toMultiset_insert toMultiset_singleton
+
+instance [ToMultiset C τ] [AgreesWithToMultiset C τ] : AgreesWithToSet C τ where
+  toSet_empty := by
+    simp [toSet, toMultiset_empty]; rfl
+  toSet_insert := by
+    intro c x
+    simp [toSet, toMultiset_insert]; rfl
+  toSet_singleton := by
     intro x
-    simp [Mem.ToMultiset.mem_iff_mem_toMultiset, ToMultiset.toMultiset_singleton]
+    simp [toSet, toMultiset_singleton]; rfl
 
-@[simp] theorem toList_empty [Membership τ C] [Mem C τ] [ToList C τ] [Mem.ToList C τ]
+@[simp] theorem toList_empty [ToList C τ] [AgreesWithToMultiset C τ]
   : toList (empty (C := C)) = [] := by
-  rw [List.eq_nil_iff_forall_not_mem]
-  intro x
-  rw [← Mem.ToList.mem_iff_mem_toList]
-  apply Mem.mem_empty
+  rw [← List.isEmpty_iff_eq_nil
+    , ← Multiset.coe_eq_zero_iff_isEmpty]
+  simp [toMultiset_empty]
 
-@[simp] theorem toList_singleton [ToList C τ] [LeanColls.ToMultiset C τ] [LawfulToList C τ] [ToMultiset C τ]
+@[simp] theorem toList_singleton [ToList C τ] [AgreesWithToMultiset C τ]
   : toList (singleton (C := C) x) = [x] := by
   apply Multiset.coe_eq_singleton.mp
-  rw [LawfulToList.toMultiset_toList]
-  rw [ToMultiset.toMultiset_singleton]
+  simp [toMultiset_singleton]
 
 def into (C' : Type u) {τ} [Insert C' τ] {C} [Fold C τ] (c : C) : C' :=
   fold c insert empty
@@ -60,21 +71,31 @@ export Insert (into)
 namespace Insert
 
 @[simp]
-theorem mem_into_iff [Insert C' τ] [Membership τ C'] [Mem C' τ]
-    [Fold C τ] [Membership τ C] [ToList C τ] [Fold.ToList C τ] [Mem.ToList C τ]
+theorem toMultiset_into_eq [ToMultiset C τ] [ToMultiset C' τ]
+    [Fold C τ] [Fold.AgreesWithToMultiset C τ]
+    [Insert C' τ] [AgreesWithToMultiset C' τ]
+    (c : C)
+  : toMultiset (into C' c) = toMultiset c := by
+  unfold into
+  apply Fold.multisetInduction c (motive := fun m acc => toMultiset acc = m)
+  · simp [toMultiset_empty]
+  · rintro _ _ _ _ _ rfl
+    simp [toMultiset_insert]
+
+@[simp]
+theorem mem_into_iff
+    [Fold C τ] [ToMultiset C τ] [Fold.AgreesWithToMultiset C τ]
+    [Insert C' τ] [ToSet C' τ] [AgreesWithToSet C' τ]
+    [Membership τ C'] [Membership.AgreesWithToSet C' τ]
+    [Membership τ C] [Membership.AgreesWithToSet C τ]
     (c : C)
   : x ∈ into C' c ↔ x ∈ c := by
   unfold into
-  have ⟨L, perm, h⟩ := Fold.ToList.fold_eq_fold_toList c
-  conv at h => ext; ext; ext; rw [← List.foldr_reverse]
-  replace perm := (List.reverse_perm ..).trans perm
-  generalize L.reverse = L' at perm h; clear L
-  conv => lhs; rw [h]
-  clear h
-  conv => rhs; rw [Mem.ToList.mem_iff_mem_toList, ← perm.mem_iff]
-  clear perm
-  induction L' with
-  | nil =>
-    simp [Mem.mem_empty]
-  | cons hd tl ih =>
-    simp [Mem.mem_insert, ih]
+  conv => rhs; rw [←Membership.mem_toMultiset_iff_mem]
+  apply Fold.multisetInduction c (motive := fun m acc => x ∈ acc ↔ x ∈ m)
+  · rw [Membership.AgreesWithToSet.mem_iff_mem_toSet, toSet_empty]
+    simp
+  · rintro _ _ _ _ _ h
+    rw [Membership.AgreesWithToSet.mem_iff_mem_toSet, toSet_insert]
+    simp [toMultiset_insert]
+    rw [h]
diff --git a/LeanColls/Classes/Seq.lean b/LeanColls/Classes/Seq.lean
index edaf41975..48790a853 100644
--- a/LeanColls/Classes/Seq.lean
+++ b/LeanColls/Classes/Seq.lean
@@ -87,10 +87,11 @@ namespace LeanColls
 
 class LawfulSeq (C : Type u) (τ : outParam (Type v)) [Seq C τ]
   extends
-    Mem.ToList C τ,
-    Append.ToList C τ,
-    Insert.ToMultiset C τ,
-    Fold.ToList C τ
+    Membership.AgreesWithToSet C τ,
+    Append.AgreesWithToList C τ,
+    Insert.AgreesWithToMultiset C τ,
+    Fold.LawfulFold C τ,
+    Fold.AgreesWithToMultiset C τ
   : Prop
   where
   size_def : ∀ (cont : C),
@@ -121,7 +122,7 @@ end LeanColls
 namespace List
 
 instance : LeanColls.LawfulSeq (List τ) τ where
-  mem_iff_mem_toList   := by simp
+  mem_iff_mem_toSet    := by intros; simp [LeanColls.instToSet_1]; rfl
   toList_append        := by simp
   toList_ofFn          := by simp
   toList_set           := by simp
@@ -137,9 +138,9 @@ instance : LeanColls.LawfulSeq (List τ) τ where
   toList_update := by intros; rfl
   toList_cons := by intros; rfl
   toList_snoc := by intros; rfl
-  fold_eq_fold_toList := by
+  exists_eq_list_foldl := by
     intro c
-    refine ⟨_, List.Perm.refl _, ?_⟩
+    refine ⟨_, rfl, ?_⟩
     intros; rfl
   foldM_eq_fold := by
     intros; simp [LeanColls.foldM, LeanColls.fold, List.foldlM_eq_foldl]
@@ -150,19 +151,17 @@ namespace LeanColls
 
 namespace Seq
 
-export Mem.ToList (
-  mem_iff_mem_toList
+export Membership.AgreesWithToSet (
+  mem_iff_mem_toSet
 )
 
-export Append.ToList (
+export Append.AgreesWithToList (
   toList_append
 )
-attribute [simp] toList_append
 
-export Insert.ToMultiset (
+export Insert.AgreesWithToMultiset (
   toMultiset_empty
 )
-attribute [simp] toMultiset_empty
 
 export LawfulSeq (
 size_def
diff --git a/LeanColls/Data/Array.lean b/LeanColls/Data/Array.lean
index 67fd074b0..8c3dfe11d 100644
--- a/LeanColls/Data/Array.lean
+++ b/LeanColls/Data/Array.lean
@@ -52,7 +52,10 @@ instance : Seq (Array α) α where
   getSnoc? := Array.getSnoc?
 
 instance : LawfulSeq (Array α) α where
-  mem_iff_mem_toList := by simp [LeanColls.toList, mem_def]
+  mem_iff_mem_toSet := by
+    simp [toSet, Set.mem_def, Array.mem_def, Membership.mem_toMultiset_iff_mem_toList]
+    simp only [← Array.toList_eq]
+    intros; rfl
   toList_append := by simp [LeanColls.toList]
   toMultiset_empty := by
     simp [LeanColls.toList, ToMultiset.toMultiset, LeanColls.empty, empty]
@@ -126,10 +129,12 @@ instance : LawfulSeq (Array α) α where
     simp [LeanColls.toList, Seq.cons, cons]
   toList_snoc := by
     simp [LeanColls.toList, Seq.snoc, snoc]
-  fold_eq_fold_toList := by
-    intro A; use A.toList; refine ⟨.rfl, ?_⟩
-    intros
-    simp [fold, foldl_eq_foldl_data]
+  exists_eq_list_foldl := by
+    intro A; use A.toList
+    constructor
+    · rfl
+    · intros
+      simp [fold, foldl_eq_foldl_data]
   foldM_eq_fold := by
     intros
     simp [fold, foldM]
@@ -152,8 +157,8 @@ instance : Fold ByteArray UInt8 where
   fold arr := arr.foldl
   foldM arr := arr.foldlM
 
-instance : Membership UInt8 ByteArray := Fold.toMem
---instance : Mem.ToList ByteArray UInt8 := Fold.toMem.ToList
+instance : Membership UInt8 ByteArray := Fold.instMem
+--instance : Membership.AgreesWithToSet ByteArray UInt8 := Fold.instMem.AgreesWithToSet
 
 instance : Seq ByteArray UInt8 where
   size := size
@@ -176,8 +181,8 @@ instance : Fold FloatArray Float where
   fold arr := arr.foldl
   foldM arr := arr.foldlM
 
-instance : Membership Float FloatArray := Fold.toMem
---instance : Mem.ToList FloatArray Float := Fold.toMem.ToList
+instance : Membership Float FloatArray := Fold.instMem
+--instance : Mem.ToList FloatArray Float := Fold.instMem.AgreesWithToSet
 
 def append (A1 A2 : FloatArray) : FloatArray :=
   aux A1 0
diff --git a/LeanColls/Data/AssocList.lean b/LeanColls/Data/AssocList.lean
index 9a2b00121..eb0d8ceb1 100644
--- a/LeanColls/Data/AssocList.lean
+++ b/LeanColls/Data/AssocList.lean
@@ -32,17 +32,19 @@ instance : Fold (AssocList κ τ) (κ × τ) where
 instance : ToList (AssocList κ τ) (κ × τ) where
   toList := Std.AssocList.toList
 
-instance : Fold.ToList (AssocList κ τ) (κ × τ) where
-  fold_eq_fold_toList := by
-    intro c
-    use c.toList
-    simp only [toList]
-    simp [fold]
+instance : Fold.LawfulFold (AssocList κ τ) (κ × τ) where
   foldM_eq_fold := by
     simp [foldM, fold]
     intros
     rw [List.foldlM_eq_foldl]
 
+instance : Fold.AgreesWithToMultiset (AssocList κ τ) (κ × τ) where
+  exists_eq_list_foldl := by
+    intro c
+    use c.toList
+    simp only [toMultiset, toList]
+    simp [fold]
+
 instance [BEq κ] : Membership (κ × τ) (AssocList κ τ) where
   mem := fun (k,t) m => m.find? k = some t
 
@@ -53,18 +55,22 @@ instance : Fold (Dict.KeySet (AssocList κ τ)) κ where
 instance : ToList (Dict.KeySet (AssocList κ τ)) (κ) where
   toList := fun ⟨al⟩ => al.toList.map (·.1)
 
-instance : Fold.ToList (Dict.KeySet (AssocList κ τ)) κ where
-  fold_eq_fold_toList := by
-    intro c
-    use c.data.toList.map (·.1)
-    simp only [toList]
-    simp [fold, List.foldl_map]
+instance : Fold.LawfulFold (Dict.KeySet (AssocList κ τ)) κ where
   foldM_eq_fold := by
     simp [foldM, fold]
     intros
     rw [List.foldlM_eq_foldl]
 
-instance [DecidableEq κ] : Membership κ (Dict.KeySet (AssocList κ τ)) := Fold.toMem
+instance [DecidableEq κ] : Membership κ (Dict.KeySet (AssocList κ τ)) := Fold.instMem
+
+instance : Fold.AgreesWithToMultiset (Dict.KeySet (AssocList κ τ)) κ where
+  exists_eq_list_foldl := by
+    intro c
+    use c.data.toList.map (·.1)
+    simp only [toMultiset, toList]
+    simp [fold, List.foldl_map]
+
+instance [DecidableEq κ] : Membership κ (Dict.KeySet (AssocList κ τ)) := Fold.instMem
 
 -- TODO(JG)
 instance [DecidableEq κ] : Dict (AssocList κ τ) κ τ where