simp only [←inst.abs_map, Container.Map]
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs { fst := n, snd := k } =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs { fst := n, snd := k }
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ abs { fst := n, snd := (fun x => Quot.mk (congr F) x) ∘ (Container.M.corec fun x => repr (f x)) ∘ k } =
    abs { fst := n, snd := (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) ∘ k }