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
case MStep
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
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
⊢ Approx.MStep nodex cx = approx y (Nat.succ n)
no goals