conv =>
  congr
  <;> rw [←inst.abs_repr x]
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> x = f <$> g <$> x
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> abs (repr x) = f <$> g <$> abs (repr x)