conv =>
  congr
  . rfl
  . rfl
  . rw [←construct_destruct x]
  . rw [←construct_destruct y]
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (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))
    x y
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₁ : x = corec (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))