simp only [destruct, corec, destruct.f, Container.M.destruct_corec, inst.abs_map, inst.abs_repr]
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ destruct (corec f x₀) = (fun x => corec f 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)) <$> f x₀ =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> f x₀