cases destruct (k r) with
| Pure r =>
  simp only [Map]
| Free n k =>
  simp only [Map]
  conv =>
    lhs
    congr
    simp only [Function.comp]
    intro x
    rw [bind_inr]
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)
no goals