Is Bisimulation trace Eq not bisim

theorem IsBisimulation.traceEq_not_bisim :    ∃ (State : Type) (Label : Type) (lts : LTS State Label),      ¬(IsHomBisimulation lts (HomTraceEq lts)) := by  let lts := LTS.mk BisimMotTr  exists ℕ, Char, lts  intro h  have htreq : (1 ~tr[lts] 5) := by    have htraces₁ : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by      ext μs      constructor      case mp =>        rintro ⟨_, (_ | ⟨⟨_⟩, (_ | ⟨(_ | _), (_ | ⟨⟨_⟩, _⟩)⟩)⟩)⟩        all_goals simp      case mpr =>        rintro (rfl | rfl | rfl | rfl)        · exact ⟨1, .refl⟩        · exact ⟨2, MTr.single lts .one2two⟩        · exact ⟨3, MTr.stepL .one2two <| MTr.single lts .two2three⟩        · exact ⟨4, MTr.stepL .one2two <| MTr.single lts .two2four⟩    have htraces₅ : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by      ext μs      constructor      case mp =>        rintro ⟨_, (_ | ⟨(_ | _), (_ | ⟨⟨_⟩, (_ | ⟨⟨_⟩, _⟩)⟩)⟩)⟩        all_goals simp      case mpr =>        rintro (rfl | rfl | rfl | rfl)        · exact ⟨5, .refl⟩        · exact ⟨6, MTr.single lts .five2six⟩        · exact ⟨7, MTr.stepL .five2six <| MTr.single lts .six2seven⟩        · exact ⟨9, MTr.stepL .five2eight <| MTr.single lts .eight2nine⟩    exact htraces₁.trans htraces₅.symm  obtain ⟨h1, h2⟩ := h htreq 'a'  obtain ⟨s₂', htr5, cih⟩ := h1 2 (by constructor)  have htraces₂ : {['b'], ['c']} ⊆ lts.traces 2 := by    intro μs h    rcases h with (rfl | rfl)    · refine ⟨3, MTr.single lts .two2three⟩    · refine ⟨4, MTr.single lts .two2four⟩  cases htr5  case five2six =>    suffices ['c'] ∉ lts.traces 6 by grind [TraceEq]    rintro ⟨_, (_ | h)⟩    cases h  case five2eight =>    suffices ['b'] ∉ lts.traces 8 by grind [TraceEq]    rintro ⟨_, (_ | h)⟩    cases h