. intro x y ⟨i, wfx, wfy, r⟩
  have ⟨⟨node, h₄⟩, k₁, k₂, h₁, h₂, h₃⟩ := h₀ i ⟨x, wfx⟩ ⟨y, wfy⟩ r
  have h₁ := lift_destruct_eq _ _ _ _ h₁
  have h₂ := lift_destruct_eq _ _ _ _ h₂
  have wfx' := wf_destruct ⟨x, wfx⟩
  have wfy' := wf_destruct ⟨y, wfy⟩
  exists node
  exists λ a => (k₁ a).1
  exists λ x => (k₂ x).1
  simp only [h₁, h₂, true_and]
  intro a
  exists C.Next node a
  simp only [toContainer] at a
  exists (by
      rw [h₁] at wfx'
      apply wfx'
    )
  exists (by
      rw [h₂] at wfy'
      apply wfy'
    )
  exact h₃ a
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∀ (x y : Container.M (toContainer C)),
    (∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }