{motive : Lean.Language.Lean.HeaderParsedSnapshot → Sort u} →
  (t : Lean.Language.Lean.HeaderParsedSnapshot) →
    ((toSnapshot : Lean.Language.Snapshot) →
        (metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf) →
          (ictx : Lean.Parser.InputContext) →
            (stx : Lean.Syntax) →
              (result? : Option Lean.Language.Lean.HeaderParsedState) →
                motive
                  { toSnapshot := toSnapshot, metaSnap := metaSnap, ictx := ictx, stx := stx, result? := result? }) →
      motive t