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
h₂ : Approx.node (approx x (Nat.succ n)) = node x
h₃ : Approx.node (approx y (Nat.succ n)) = node y
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
no goals