case succ n h =>
  have h₂ := x.node_thm n
  have h₃ := y.node_thm n
  cases h₄: x.approx (.succ n) with
  | MStep nodex cx =>
    cases h₅: y.approx (.succ n) with
    | MStep nodey cy =>
      have ⟨node, k₁, k₂, eq₁, eq₂, kR⟩ := h₀ _ _ h₁
      have h₂ : (Approx.MStep nodex cx).node = node := by
        have := congrArg (λ x => x.1) eq₁
        simp only [destruct] at this
        rw [h₄] at h₂
        rw [←this]
        exact h₂
      have h₃ : (Approx.MStep nodey cy).node = node := by
        have := congrArg (λ x => x.1) eq₂
        simp only [destruct] at this
        rw [h₅] at h₃
        rw [←this]
        exact h₃
      simp [Approx.node] at h₂ h₃
      have h₂ := Eq.symm h₂
      have h₃ := Eq.symm h₃
      have h₆ := bisim.lemma0 x n
      have h₇ := bisim.lemma0 y n
      rw [h₄] at h₆
      rw [h₅] at h₇
      simp only [Approx.children] at h₇ h₆
      induction h₂
      induction h₃
      suffices h₈ : ∀ i: C.B node, cx i = cy i by
        have : cx = cy := by
          funext i
          apply h₈
        rw [this]
      intro i
      have h₆ : ∀ i, cx i = (k₁ i).approx n := by
        have h : ∀ i j, HEq i j → (x.destruct.snd i) = k₁ j := by
          rw [eq₁]
          intro i j heq
          cases heq
          rfl
        intro i
        rw [h₆ i (cast (by simp [congrArg (λ x => x.1) eq₁]) i)]
        . rw [h]
          apply cast_heq
        . apply HEq.symm
          apply cast_heq
      have h₇ : ∀ i, cy i = (k₂ i).approx n := by
        have h : ∀ i j, HEq i j → (y.destruct.snd i) = k₂ j := by
          rw [eq₂]
          intro i j heq
          cases heq
          rfl
        intro i
        rw [h₇ i (cast (by simp [congrArg (λ x => x.1) eq₂]) i)]
        . rw [h]
          apply cast_heq
        . apply HEq.symm
          apply cast_heq
      rw [h₆, h₇]
      apply h
      apply kR
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)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
no goals