{motive : Lean.Elab.Tactic.TacticFinishedSnapshot → Sort u} →
  (t : Lean.Elab.Tactic.TacticFinishedSnapshot) →
    ((toSnapshot : Lean.Language.Snapshot) →
        (state? : Option Lean.Elab.Tactic.SavedState) →
          (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
            motive { toSnapshot := toSnapshot, state? := state?, moreSnaps := moreSnaps }) →
      motive t