conv =>
  congr
  <;> rw [←inst.abs_repr x]
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
⊢ IFunctor.imap (fun i => f i ∘ g i) x = IFunctor.imap f (IFunctor.imap g x)
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
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs (repr x)) = IFunctor.imap f (IFunctor.imap g (abs (repr x)))