-- Init.Grind.Config
Lean.Grind.Config.mk.injEq : ∀ (trace markInstances lax suggestions locals : Bool) (splits ematch gen genLocal instances : ℕ)
  (matchEqs splitMatch splitIte splitIndPred splitImp : Bool) (canonHeartbeats : ℕ)
  (ext extAll etaStruct funext lookahead verbose clean qlia mbtc zetaDelta zeta ring : Bool)
  (ringSteps ringMaxDegree : ℕ) (linarith lia : Bool) (liaSteps : ℕ) (ac : Bool) (acSteps exp : ℕ)
  (abstractProof inj order : Bool) (min detailed : ℕ) (useSorry revert funCC reducible : Bool)
  (maxSuggestions : Option ℕ) (trace_1 markInstances_1 lax_1 suggestions_1 locals_1 : Bool)
  (splits_1 ematch_1 gen_1 genLocal_1 instances_1 : ℕ)
  (matchEqs_1 splitMatch_1 splitIte_1 splitIndPred_1 splitImp_1 : Bool) (canonHeartbeats_1 : ℕ)
  (ext_1 extAll_1 etaStruct_1 funext_1 lookahead_1 verbose_1 clean_1 qlia_1 mbtc_1 zetaDelta_1 zeta_1 ring_1 : Bool)
  (ringSteps_1 ringMaxDegree_1 : ℕ) (linarith_1 lia_1 : Bool) (liaSteps_1 : ℕ) (ac_1 : Bool) (acSteps_1 exp_1 : ℕ)
  (abstractProof_1 inj_1 order_1 : Bool) (min_1 detailed_1 : ℕ) (useSorry_1 revert_1 funCC_1 reducible_1 : Bool)
  (maxSuggestions_1 : Option ℕ),
  ({ trace := trace, markInstances := markInstances, lax := lax, suggestions := suggestions, locals := locals,
        splits := splits, ematch := ematch, gen := gen, genLocal := genLocal, instances := instances,
        matchEqs := matchEqs, splitMatch := splitMatch, splitIte := splitIte, splitIndPred := splitIndPred,
        splitImp := splitImp, canonHeartbeats := canonHeartbeats, ext := ext, extAll := extAll, etaStruct := etaStruct,
        funext := funext, lookahead := lookahead, verbose := verbose, clean := clean, qlia := qlia, mbtc := mbtc,
        zetaDelta := zetaDelta, zeta := zeta, ring := ring, ringSteps := ringSteps, ringMaxDegree := ringMaxDegree,
        linarith := linarith, lia := lia, liaSteps := liaSteps, ac := ac, acSteps := acSteps, exp := exp,
        abstractProof := abstractProof, inj := inj, order := order, min := min, detailed := detailed,
        useSorry := useSorry, revert := revert, funCC := funCC, reducible := reducible,
        maxSuggestions := maxSuggestions } =
      { trace := trace_1, markInstances := markInstances_1, lax := lax_1, suggestions := suggestions_1,
        locals := locals_1, splits := splits_1, ematch := ematch_1, gen := gen_1, genLocal := genLocal_1,
        instances := instances_1, matchEqs := matchEqs_1, splitMatch := splitMatch_1, splitIte := splitIte_1,
        splitIndPred := splitIndPred_1, splitImp := splitImp_1, canonHeartbeats := canonHeartbeats_1, ext := ext_1,
        extAll := extAll_1, etaStruct := etaStruct_1, funext := funext_1, lookahead := lookahead_1,
        verbose := verbose_1, clean := clean_1, qlia := qlia_1, mbtc := mbtc_1, zetaDelta := zetaDelta_1,
        zeta := zeta_1, ring := ring_1, ringSteps := ringSteps_1, ringMaxDegree := ringMaxDegree_1,
        linarith := linarith_1, lia := lia_1, liaSteps := liaSteps_1, ac := ac_1, acSteps := acSteps_1, exp := exp_1,
        abstractProof := abstractProof_1, inj := inj_1, order := order_1, min := min_1, detailed := detailed_1,
        useSorry := useSorry_1, revert := revert_1, funCC := funCC_1, reducible := reducible_1,
        maxSuggestions := maxSuggestions_1 }) =
    (trace = trace_1 ∧
      markInstances = markInstances_1 ∧
        lax = lax_1 ∧
          suggestions = suggestions_1 ∧
            locals = locals_1 ∧
              splits = splits_1 ∧
                ematch = ematch_1 ∧
                  gen = gen_1 ∧
                    genLocal = genLocal_1 ∧
                      instances = instances_1 ∧
                        matchEqs = matchEqs_1 ∧
                          splitMatch = splitMatch_1 ∧
                            splitIte = splitIte_1 ∧
                              splitIndPred = splitIndPred_1 ∧
                                splitImp = splitImp_1 ∧
                                  canonHeartbeats = canonHeartbeats_1 ∧
                                    ext = ext_1 ∧
                                      extAll = extAll_1 ∧
                                        etaStruct = etaStruct_1 ∧
                                          funext = funext_1 ∧ lookahead = lookahead_1 ∧ verbose = verbose_1 ∧ ⋯)