cases hy: destruct y with
| Pure r =>
  simp only [Map, hy, bind.automaton] at h₂
  rw [h₂]
  apply equivF.Pure
  rfl
| Free n k =>
  simp only [Map, bind.automaton, hy] at h₂
  rw [h₂]
  apply equivF.Free
  intro y
  left
  rfl
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = Map (corec (bind.automaton f)) (bind.automaton f (Sum.inr y))
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct (destruct x)) (construct (destruct y))
no goals