cases h₁ with
| Pure x y h₁ =>
  induction h₁
  exists (A.Pure x)
  exists (λ e => e.casesOn)
  exists (λ e => e.casesOn)
  simp only [construct, M.destruct_construct, inv, true_and]
  intro x
  apply x.elim
| Free node k₁ k₂ h =>
  exists (A.Free node)
  exists k₁
  exists k₂
  simp only [construct, M.destruct_construct, inv, true_and]
  intro x
  rw [CompleteLattice.bot_sup] at h
  apply h
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : ↑(equivF' Eq) (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) x y
⊢ ∃ node k₁ k₂,
    M.destruct x = { fst := node, snd := k₁ } ∧
      M.destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : Container.B (Container C R) node), eq (k₁ i) (k₂ i)
no goals