m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
l : AssocList α β
init : δ
f : α × β → δ → m (ForInStep δ)
⊢ AssocList.forIn l init f = List.forIn.loop f (toList l) init
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
l : AssocList α β
init : δ
f : α × β → δ → m (ForInStep δ)
⊢ forIn l init f = forIn (toList l) init f
simp [forIn, List.forIn]
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), AssocList.forIn tail✝ init f = List.forIn.loop f (toList tail✝) init
init : δ
⊢ (do
      let __do_lift ← f (key✝, value✝) init
      match __do_lift with
        | ForInStep.done d => pure d
        | ForInStep.yield d => AssocList.forIn tail✝ d f) =
    do
    let __do_lift ← f (key✝, value✝) init
    match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield b => List.forIn.loop f (toList tail✝) b
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
l : AssocList α β
init : δ
f : α × β → δ → m (ForInStep δ)
⊢ AssocList.forIn l init f = List.forIn.loop f (toList l) init
induction l generalizing init <;> simp [AssocList.forIn, List.forIn.loop]
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), AssocList.forIn tail✝ init f = List.forIn.loop f (toList tail✝) init
init : δ
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => AssocList.forIn tail✝ d f) =
    fun __do_lift =>
    match __do_lift with
    | ForInStep.done d => pure d
    | ForInStep.yield b => List.forIn.loop f (toList tail✝) b
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), AssocList.forIn tail✝ init f = List.forIn.loop f (toList tail✝) init
init : δ
⊢ (do
      let __do_lift ← f (key✝, value✝) init
      match __do_lift with
        | ForInStep.done d => pure d
        | ForInStep.yield d => AssocList.forIn tail✝ d f) =
    do
    let __do_lift ← f (key✝, value✝) init
    match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield b => List.forIn.loop f (toList tail✝) b
congr
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), AssocList.forIn tail✝ init f = List.forIn.loop f (toList tail✝) init
init : δ
a : ForInStep δ
⊢ (match a with
    | ForInStep.done d => pure d
    | ForInStep.yield d => AssocList.forIn tail✝ d f) =
    match a with
    | ForInStep.done d => pure d
    | ForInStep.yield b => List.forIn.loop f (toList tail✝) b
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), AssocList.forIn tail✝ init f = List.forIn.loop f (toList tail✝) init
init : δ
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => AssocList.forIn tail✝ d f) =
    fun __do_lift =>
    match __do_lift with
    | ForInStep.done d => pure d
    | ForInStep.yield b => List.forIn.loop f (toList tail✝) b
funext a
no goals
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), AssocList.forIn tail✝ init f = List.forIn.loop f (toList tail✝) init
init : δ
a : ForInStep δ
⊢ (match a with
    | ForInStep.done d => pure d
    | ForInStep.yield d => AssocList.forIn tail✝ d f) =
    match a with
    | ForInStep.done d => pure d
    | ForInStep.yield b => List.forIn.loop f (toList tail✝) b
split <;> simp [*]