apply Free.equiv.coinduction
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ ∀ (x y : Free C S),
    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