cases repr (f i x₀) with
| mk n k =>
  simp only [←inst.abs_imap, IContainer.Map]
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs (repr (f i x₀)))) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs (repr (f i x₀)))
no goals