∀ (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))
  (toSnapshot_1 : Lean.Language.Snapshot) (stx_1 : Lean.Syntax) (parserState_1 : Lean.Parser.ModuleParserState)
  (elabSnap_1 : Lean.Language.Lean.CommandElaboratingSnapshot)
  (nextCmdSnap?_1 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)),
  ({ toSnapshot := toSnapshot, stx := stx, parserState := parserState, elabSnap := elabSnap,
        nextCmdSnap? := nextCmdSnap? } =
      { toSnapshot := toSnapshot_1, stx := stx_1, parserState := parserState_1, elabSnap := elabSnap_1,
        nextCmdSnap? := nextCmdSnap?_1 }) =
    (toSnapshot = toSnapshot_1 ∧
      stx = stx_1 ∧ parserState = parserState_1 ∧ elabSnap = elabSnap_1 ∧ nextCmdSnap? = nextCmdSnap?_1)