clear h₁
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)
h₂ : destruct x = destruct (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))
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y : Free C S
h₂ : destruct x = destruct (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))