{motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u} →
    {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
      {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
        (t : Lean.Language.Lean.CommandParsedSnapshot) →
          ((toSnapshot : Lean.Language.Snapshot) →
              (stx : Lean.Syntax) →
                (parserState : Lean.Parser.ModuleParserState) →
                  (elabSnap : Lean.Language.Lean.CommandElaboratingSnapshot) →
                    (nextCmdSnap? : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
                      motive_2 nextCmdSnap? →
                        motive_1
                          { toSnapshot := toSnapshot, stx := stx, parserState := parserState, elabSnap := elabSnap,
                            nextCmdSnap? := nextCmdSnap? }) →
            motive_2 none →
              ((val : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
                  motive_3 val → motive_2 (some val)) →
                ((stx? : Option Lean.Syntax) →
                    (reportingRange : Lean.Language.SnapshotTask.ReportingRange) →
                      (cancelTk? : Option IO.CancelToken) →
                        (task : Task Lean.Language.Lean.CommandParsedSnapshot) →
                          motive_4 task →
                            motive_3
                              { stx? := stx?, reportingRange := reportingRange, cancelTk? := cancelTk?,
                                task := task }) →
                  ((get : Lean.Language.Lean.CommandParsedSnapshot) → motive_1 get → motive_4 { get := get }) →
                    motive_1 t