∀ (fileName : String) (fileMap : Lean.FileMap) (currRecDepth : ℕ) (cmdPos : String.Pos.Raw)
  (macroStack : Lean.Elab.MacroStack) (quotContext? : Option Lean.Name) (currMacroScope : Lean.MacroScope)
  (ref : Lean.Syntax) (snap? : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot))
  (cancelTk? : Option IO.CancelToken) (suppressElabErrors : Bool) (fileName_1 : String) (fileMap_1 : Lean.FileMap)
  (currRecDepth_1 : ℕ) (cmdPos_1 : String.Pos.Raw) (macroStack_1 : Lean.Elab.MacroStack)
  (quotContext?_1 : Option Lean.Name) (currMacroScope_1 : Lean.MacroScope) (ref_1 : Lean.Syntax)
  (snap?_1 : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot)) (cancelTk?_1 : Option IO.CancelToken)
  (suppressElabErrors_1 : Bool),
  ({ fileName := fileName, fileMap := fileMap, currRecDepth := currRecDepth, cmdPos := cmdPos, macroStack := macroStack,
        quotContext? := quotContext?, currMacroScope := currMacroScope, ref := ref, snap? := snap?,
        cancelTk? := cancelTk?, suppressElabErrors := suppressElabErrors } =
      { fileName := fileName_1, fileMap := fileMap_1, currRecDepth := currRecDepth_1, cmdPos := cmdPos_1,
        macroStack := macroStack_1, quotContext? := quotContext?_1, currMacroScope := currMacroScope_1, ref := ref_1,
        snap? := snap?_1, cancelTk? := cancelTk?_1, suppressElabErrors := suppressElabErrors_1 }) =
    (fileName = fileName_1 ∧
      fileMap = fileMap_1 ∧
        currRecDepth = currRecDepth_1 ∧
          cmdPos = cmdPos_1 ∧
            macroStack = macroStack_1 ∧
              quotContext? = quotContext?_1 ∧
                currMacroScope = currMacroScope_1 ∧
                  ref = ref_1 ∧ snap? = snap?_1 ∧ cancelTk? = cancelTk?_1 ∧ suppressElabErrors = suppressElabErrors_1)