have : ∀ (x y:Free C R), x = y → Free.eq x y := by
  apply Free.equiv.coinduction
  intro x y h
  cases h
  conv =>
    congr
    . rfl
    . rfl
    . rw [←construct_destruct x]
    . rw [←construct_destruct x]
  cases destruct x with
  | Pure r =>
    apply equivF.Pure
    rfl
  | Free node k =>
    apply equivF.Free
    intro y
    left
    rfl
C : _root_.Container
R : Type u₁
⊢ ∀ (x : Free C R), eq x x
C : _root_.Container
R : Type u₁
this : ∀ (x y : Free C R), x = y → eq x y
⊢ ∀ (x : Free C R), eq x x