simp only [Map]
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Map (corec (bind.automaton k✝)) (Map Sum.inr (Functor.Free n k)) = Functor.Free n k
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Functor.Free n (corec (bind.automaton k✝) ∘ Sum.inr ∘ k) = Functor.Free n k