simp [←inst.abs_map, Container.Map]
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ (f ∘ g) <$> abs { fst := fst✝, snd := snd✝ } = f <$> g <$> abs { fst := fst✝, snd := snd✝ }
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ abs { fst := fst✝, snd := (f ∘ g) ∘ snd✝ } = abs { fst := fst✝, snd := f ∘ g ∘ snd✝ }