cases destruct x with
| Pure r =>
  apply equivF.Pure
  rfl
| Free node k =>
  apply equivF.Free
  intro y
  left
  rfl
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (construct (destruct x)) (construct (destruct x))
no goals