intro x y h₁
case h₀
C : _root_.Container
R : Type u₁
⊢ ∀ (x y : M (Container C R)),
    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₁ : 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)