Saturate m Tr s MTr not nil iff

@[scoped grind =]theorem saturate_mTr_sMTr_not_nil_iff [HasTau Label] {lts : LTS State Label}    (hμs : μs ≠ []) : lts.saturate.MTr s μs s' ↔ lts.SMTr s μs s' := by  induction μs generalizing s  case nil => contradiction  case cons x xs ih =>    apply Iff.intro <;> intro h    case mp =>      cases h      case stepL sb htr hmtr =>        cases xs with        | nil =>          cases hmtr          apply LTS.SMTr.stepL htr (by grind only [SMTr.fromMTr, MTr.refl])        | cons x' xs' =>          exact LTS.SMTr.stepL htr ((ih (by simp)).mp hmtr)    case mpr =>      cases h      case stepL sb htr hmtr =>        cases xs with        | nil =>          cases hmtr          case τ h_τ =>            exact LTS.MTr.stepL              (LTS.STr.comp LTS.STr.refl htr h_τ)              LTS.MTr.refl        | cons x' xs' =>          exact LTS.MTr.stepL htr ((ih (by simp)).mpr hmtr)