simp only [Map, hy, bind.automaton] at h₂
case a.Pure
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))
r : S
hy : destruct y = Functor.Pure r
⊢ 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 (Functor.Pure r))
case a.Pure
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
r : S
hy : destruct y = Functor.Pure r
h₂ : destruct x = Functor.Pure r
⊢ 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 (Functor.Pure r))