∀ (mctx : Lean.MetavarContext) (nextMacroScope : Lean.MacroScope) (ngen : Lean.NameGenerator)
  (cache : Std.HashMap Lean.ExprStructEq Lean.Expr) (mctx_1 : Lean.MetavarContext) (nextMacroScope_1 : Lean.MacroScope)
  (ngen_1 : Lean.NameGenerator) (cache_1 : Std.HashMap Lean.ExprStructEq Lean.Expr),
  ({ mctx := mctx, nextMacroScope := nextMacroScope, ngen := ngen, cache := cache } =
      { mctx := mctx_1, nextMacroScope := nextMacroScope_1, ngen := ngen_1, cache := cache_1 }) =
    (mctx = mctx_1 ∧ nextMacroScope = nextMacroScope_1 ∧ ngen = ngen_1 ∧ cache = cache_1)