conv =>
  lhs
  congr
  . rfl
  . simp only [bind.automaton, destruct_construct]
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (bind.automaton k (Sum.inl (construct (Functor.Pure r)))) = destruct (k r)
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ Map (corec (bind.automaton k)) (Map Sum.inr (destruct (k r))) = destruct (k r)