simp only [IQPF.M.destruct, IQPF.M.corec, destruct.f, IContainer.M.destruct_corec, inst.abs_imap, inst.abs_repr]
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
⊢ destruct (corec f x₀) = IFunctor.imap (fun i x => corec f x) (f i x₀)
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)) (f i x₀)) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x)) (f i x₀)