cases repr (f x₀) with
| mk n k =>
  simp only [←inst.abs_map, Container.Map]
  rfl
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs (repr (f x₀)) =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs (repr (f x₀))
no goals