intro x y n h₁
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
⊢ ∀ (x y : M C) (n : Nat), R x y → approx x n = approx y n
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
n : Nat
h₁ : R x y
⊢ approx x n = approx y n