case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (do
      let x ← f head✝ init
      match x with
        | ForInStep.done b => pure b
        | ForInStep.yield b => do
          let a ← ForInStep.bindList f tail✝ (ForInStep.yield b)
          pure (ForInStep.run a)) =
    do
    let x ← f head✝ init
    let a ← ForInStep.bindList f tail✝ x
    pure (ForInStep.run a)
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
l : List α
init : β
⊢ forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
induction l generalizing init <;> simp [*, map_eq_pure_bind]
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => do
        let a ← ForInStep.bindList f tail✝ (ForInStep.yield b)
        pure (ForInStep.run a)) =
    fun x => do
    let a ← ForInStep.bindList f tail✝ x
    pure (ForInStep.run a)
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (do
      let x ← f head✝ init
      match x with
        | ForInStep.done b => pure b
        | ForInStep.yield b => do
          let a ← ForInStep.bindList f tail✝ (ForInStep.yield b)
          pure (ForInStep.run a)) =
    do
    let x ← f head✝ init
    let a ← ForInStep.bindList f tail✝ x
    pure (ForInStep.run a)
congr
no goals
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => do
        let a ← ForInStep.bindList f tail✝ (ForInStep.yield b)
        pure (ForInStep.run a)) =
    fun x => do
    let a ← ForInStep.bindList f tail✝ x
    pure (ForInStep.run a)
ext (b | b) <;> simp