have : ∀ x y, x = corec (bind.automaton f) (.inr y) → eq x y := by
  apply Free.equiv.coinduction
  intro x y h₁
  conv =>
    congr
    . rfl
    . rfl
    . rw [←construct_destruct x]
    . rw [←construct_destruct y]
  have h₂ := congrArg destruct h₁
  clear h₁
  rw [destruct_corec] at h₂
  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 : Free C S
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
this : ∀ (x y : Free C S), x = corec (bind.automaton f) (Sum.inr y) → eq x y
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x