simp [←inst.abs_imap, IContainer.Map]
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : F α i
fst✝ : IContainer.A (C F) i
snd✝ : (y : IContainer.B (C F) i fst✝) → α (IContainer.N (C F) i fst✝ y)
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs { fst := fst✝, snd := snd✝ }) =
    IFunctor.imap f (IFunctor.imap g (abs { fst := fst✝, snd := snd✝ }))
no goals