cases repr 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)
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✝ }