rw [←pgfp.unfold] at h₁
case h₀
C : _root_.Container
R : Type u₁
x y : M (Container C R)
h₁ : ↑(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)
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)