{motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  (t : Lean.Elab.Tactic.TacticParsedSnapshot) →
    ((toSnapshot : Lean.Language.Snapshot) →
        (stx : Lean.Syntax) →
          (inner? : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
            (finished : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot) →
              (next : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                motive_1
                  { toSnapshot := toSnapshot, stx := stx, inner? := inner?, finished := finished, next := next }) →
      motive_1 t