rw [←inst.abs_repr (f x₀)]
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)) <$> f x₀ =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> f x₀
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₀))