diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index 68f4fa27b0..79b8148c66 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -51,14 +51,14 @@ match s.map.find? fvarId with
 def apply (s : FVarSubst) (e : Expr) : Expr :=
 if s.map.isEmpty then e
 else if !e.hasFVar then e
-else e.replace $ fun e => match e with
+else e.replace fun e => match e with
   | Expr.fvar fvarId _ => match s.map.find? fvarId with
     | none   => e
     | some v => v
   | _ => none
 
 def domain (s : FVarSubst) : List FVarId :=
-s.map.foldl (fun r k v => k :: r) []
+s.map.foldl (init := []) fun r k v => k :: r
 
 def any (p : FVarId → Expr → Bool) (s : FVarSubst) : Bool :=
 s.map.any p
diff --git a/src/Std/Data/AssocList.lean b/src/Std/Data/AssocList.lean
index fe8271645b..3e54350321 100644
--- a/src/Std/Data/AssocList.lean
+++ b/src/Std/Data/AssocList.lean
@@ -1,15 +1,16 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
+universes u v w w'
 namespace Std
-universes u v w
 
 /- List-like type to avoid extra level of indirection -/
 inductive AssocList (α : Type u) (β : Type v)
-| nil : AssocList
-| cons (key : α) (value : β) (tail : AssocList) : AssocList
+| nil : AssocList α β
+| cons (key : α) (value : β) (tail : AssocList α β) : AssocList α β
 
 namespace AssocList
 variables {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m]
@@ -26,56 +27,69 @@ def isEmpty : AssocList α β → Bool
 | nil => true
 | _   => false
 
-@[specialize] def foldlM (f : δ → α → β → m δ) : δ → AssocList α β → m δ
+@[specialize] def foldlM (f : δ → α → β → m δ) : (init : δ) → AssocList α β → m δ
 | d, nil         => pure d
-| d, cons a b es => do d ← f d a b; foldlM d es
+| d, cons a b es => do d ← f d a b; foldlM f d es
 
-@[inline] def foldl (f : δ → α → β → δ) (d : δ) (as : AssocList α β) : δ :=
-Id.run (foldlM f d as)
+@[inline] def foldl (f : δ → α → β → δ) (init : δ) (as : AssocList α β) : δ :=
+Id.run (foldlM f init as)
 
 def mapKey (f : α → δ) : AssocList α β → AssocList δ β
 | nil        => nil
-| cons k v t => cons (f k) v (mapKey t)
+| cons k v t => cons (f k) v (mapKey f t)
 
 def mapVal (f : β → δ) : AssocList α β → AssocList α δ
 | nil        => nil
-| cons k v t => cons k (f v) (mapVal t)
+| cons k v t => cons k (f v) (mapVal f t)
 
 def findEntry? [HasBeq α] (a : α) : AssocList α β → Option (α × β)
 | nil         => none
 | cons k v es => match k == a with
   | true  => some (k, v)
-  | false => findEntry? es
+  | false => findEntry? a es
 
 def find? [HasBeq α] (a : α) : AssocList α β → Option β
 | nil         => none
 | cons k v es => match k == a with
   | true  => some v
-  | false => find? es
+  | false => find? a es
 
 def contains [HasBeq α] (a : α) : AssocList α β → Bool
 | nil         => false
-| cons k v es => k == a || contains es
+| cons k v es => k == a || contains a es
 
 def replace [HasBeq α] (a : α) (b : β) : AssocList α β → AssocList α β
 | nil         => nil
 | cons k v es => match k == a with
   | true  => cons a b es
-  | false => cons k v (replace es)
+  | false => cons k v (replace a b es)
 
 def erase [HasBeq α] (a : α) : AssocList α β → AssocList α β
 | nil         => nil
 | cons k v es => match k == a with
   | true  => es
-  | false => cons k v (erase es)
+  | false => cons k v (erase a es)
 
 def any (p : α → β → Bool) : AssocList α β → Bool
 | nil         => false
-| cons k v es => p k v || any es
+| cons k v es => p k v || any p es
 
 def all (p : α → β → Bool) : AssocList α β → Bool
 | nil         => true
-| cons k v es => p k v && all es
+| cons k v es => p k v && all p es
 
-end AssocList
-end Std
+@[inline] def forIn {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m]
+    (as : AssocList α β) (init : δ) (f : (α × β) → δ → m (ForInStep δ)) : m δ :=
+let rec @[specialize] loop
+  | d, nil => pure d
+  | d, cons k v es => do
+    match (← f (k, v) d) with
+    | ForInStep.done d  => pure d
+    | ForInStep.yield d => loop d es
+loop init as
+
+end Std.AssocList
+
+def List.toAssocList {α : Type u} {β : Type v} : List (α × β) → Std.AssocList α β
+| []          => Std.AssocList.nil
+| (a,b) :: es => Std.AssocList.cons a b (toAssocList es)