-- Init.MetaTypes
Lean.Meta.Simp.Config.mk.injEq : ∀ (maxSteps maxDischargeDepth : ℕ) (contextual memoize singlePass zeta beta eta : Bool)
  (etaStruct : Lean.Meta.EtaStructMode)
  (iota proj decide arith autoUnfold dsimp failIfUnchanged ground unfoldPartialApp zetaDelta index implicitDefEqProofs
    zetaUnused catchRuntime zetaHave letToHave congrConsts bitVecOfNat warnExponents suggestions : Bool)
  (maxSuggestions : Option ℕ) (locals instances : Bool) (maxSteps_1 maxDischargeDepth_1 : ℕ)
  (contextual_1 memoize_1 singlePass_1 zeta_1 beta_1 eta_1 : Bool) (etaStruct_1 : Lean.Meta.EtaStructMode)
  (iota_1 proj_1 decide_1 arith_1 autoUnfold_1 dsimp_1 failIfUnchanged_1 ground_1 unfoldPartialApp_1 zetaDelta_1 index_1
    implicitDefEqProofs_1 zetaUnused_1 catchRuntime_1 zetaHave_1 letToHave_1 congrConsts_1 bitVecOfNat_1 warnExponents_1
    suggestions_1 : Bool)
  (maxSuggestions_1 : Option ℕ) (locals_1 instances_1 : Bool),
  ({ maxSteps := maxSteps, maxDischargeDepth := maxDischargeDepth, contextual := contextual, memoize := memoize,
        singlePass := singlePass, zeta := zeta, beta := beta, eta := eta, etaStruct := etaStruct, iota := iota,
        proj := proj, decide := decide, arith := arith, autoUnfold := autoUnfold, dsimp := dsimp,
        failIfUnchanged := failIfUnchanged, ground := ground, unfoldPartialApp := unfoldPartialApp,
        zetaDelta := zetaDelta, index := index, implicitDefEqProofs := implicitDefEqProofs, zetaUnused := zetaUnused,
        catchRuntime := catchRuntime, zetaHave := zetaHave, letToHave := letToHave, congrConsts := congrConsts,
        bitVecOfNat := bitVecOfNat, warnExponents := warnExponents, suggestions := suggestions,
        maxSuggestions := maxSuggestions, locals := locals, instances := instances } =
      { maxSteps := maxSteps_1, maxDischargeDepth := maxDischargeDepth_1, contextual := contextual_1,
        memoize := memoize_1, singlePass := singlePass_1, zeta := zeta_1, beta := beta_1, eta := eta_1,
        etaStruct := etaStruct_1, iota := iota_1, proj := proj_1, decide := decide_1, arith := arith_1,
        autoUnfold := autoUnfold_1, dsimp := dsimp_1, failIfUnchanged := failIfUnchanged_1, ground := ground_1,
        unfoldPartialApp := unfoldPartialApp_1, zetaDelta := zetaDelta_1, index := index_1,
        implicitDefEqProofs := implicitDefEqProofs_1, zetaUnused := zetaUnused_1, catchRuntime := catchRuntime_1,
        zetaHave := zetaHave_1, letToHave := letToHave_1, congrConsts := congrConsts_1, bitVecOfNat := bitVecOfNat_1,
        warnExponents := warnExponents_1, suggestions := suggestions_1, maxSuggestions := maxSuggestions_1,
        locals := locals_1, instances := instances_1 }) =
    (maxSteps = maxSteps_1 ∧
      maxDischargeDepth = maxDischargeDepth_1 ∧
        contextual = contextual_1 ∧
          memoize = memoize_1 ∧
            singlePass = singlePass_1 ∧
              zeta = zeta_1 ∧
                beta = beta_1 ∧
                  eta = eta_1 ∧
                    etaStruct = etaStruct_1 ∧
                      iota = iota_1 ∧
                        proj = proj_1 ∧
                          decide = decide_1 ∧
                            arith = arith_1 ∧
                              autoUnfold = autoUnfold_1 ∧
                                dsimp = dsimp_1 ∧
                                  failIfUnchanged = failIfUnchanged_1 ∧
                                    ground = ground_1 ∧
                                      unfoldPartialApp = unfoldPartialApp_1 ∧
                                        zetaDelta = zetaDelta_1 ∧
                                          index = index_1 ∧
                                            implicitDefEqProofs = implicitDefEqProofs_1 ∧
                                              zetaUnused = zetaUnused_1 ∧
                                                catchRuntime = catchRuntime_1 ∧
                                                  zetaHave = zetaHave_1 ∧
                                                    letToHave = letToHave_1 ∧
                                                      congrConsts = congrConsts_1 ∧
                                                        bitVecOfNat = bitVecOfNat_1 ∧
                                                          warnExponents = warnExponents_1 ∧
                                                            suggestions = suggestions_1 ∧
                                                              maxSuggestions = maxSuggestions_1 ∧
                                                                locals = locals_1 ∧ instances = instances_1)