-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.mk.injEq : ∀ (declName? : Option Lean.Name) (macroStack : Lean.Elab.MacroStack) (mayPostpone errToSorry : Bool)
  (autoBoundImplicitContext : Option Lean.Elab.AutoBoundImplicitContext) (autoBoundImplicitForbidden : Lean.Name → Bool)
  (sectionVars : Lean.NameMap Lean.Name) (sectionFVars : Lean.NameMap Lean.Expr)
  (implicitLambda heedElabAsElim isNoncomputableSection isMetaSection ignoreTCFailures inPattern : Bool)
  (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot))
  (saveRecAppSyntax holesAsSyntheticOpaque checkDeprecated : Bool)
  (fixedTermElabs : Array Lean.Elab.Term.FixedTermElabRef) (declName?_1 : Option Lean.Name)
  (macroStack_1 : Lean.Elab.MacroStack) (mayPostpone_1 errToSorry_1 : Bool)
  (autoBoundImplicitContext_1 : Option Lean.Elab.AutoBoundImplicitContext)
  (autoBoundImplicitForbidden_1 : Lean.Name → Bool) (sectionVars_1 : Lean.NameMap Lean.Name)
  (sectionFVars_1 : Lean.NameMap Lean.Expr)
  (implicitLambda_1 heedElabAsElim_1 isNoncomputableSection_1 isMetaSection_1 ignoreTCFailures_1 inPattern_1 : Bool)
  (tacSnap?_1 : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot))
  (saveRecAppSyntax_1 holesAsSyntheticOpaque_1 checkDeprecated_1 : Bool)
  (fixedTermElabs_1 : Array Lean.Elab.Term.FixedTermElabRef),
  ({ declName? := declName?, macroStack := macroStack, mayPostpone := mayPostpone, errToSorry := errToSorry,
        autoBoundImplicitContext := autoBoundImplicitContext, autoBoundImplicitForbidden := autoBoundImplicitForbidden,
        sectionVars := sectionVars, sectionFVars := sectionFVars, implicitLambda := implicitLambda,
        heedElabAsElim := heedElabAsElim, isNoncomputableSection := isNoncomputableSection,
        isMetaSection := isMetaSection, ignoreTCFailures := ignoreTCFailures, inPattern := inPattern,
        tacSnap? := tacSnap?, saveRecAppSyntax := saveRecAppSyntax, holesAsSyntheticOpaque := holesAsSyntheticOpaque,
        checkDeprecated := checkDeprecated, fixedTermElabs := fixedTermElabs } =
      { declName? := declName?_1, macroStack := macroStack_1, mayPostpone := mayPostpone_1, errToSorry := errToSorry_1,
        autoBoundImplicitContext := autoBoundImplicitContext_1,
        autoBoundImplicitForbidden := autoBoundImplicitForbidden_1, sectionVars := sectionVars_1,
        sectionFVars := sectionFVars_1, implicitLambda := implicitLambda_1, heedElabAsElim := heedElabAsElim_1,
        isNoncomputableSection := isNoncomputableSection_1, isMetaSection := isMetaSection_1,
        ignoreTCFailures := ignoreTCFailures_1, inPattern := inPattern_1, tacSnap? := tacSnap?_1,
        saveRecAppSyntax := saveRecAppSyntax_1, holesAsSyntheticOpaque := holesAsSyntheticOpaque_1,
        checkDeprecated := checkDeprecated_1, fixedTermElabs := fixedTermElabs_1 }) =
    (declName? = declName?_1 ∧
      macroStack = macroStack_1 ∧
        mayPostpone = mayPostpone_1 ∧
          errToSorry = errToSorry_1 ∧
            autoBoundImplicitContext = autoBoundImplicitContext_1 ∧
              autoBoundImplicitForbidden = autoBoundImplicitForbidden_1 ∧
                sectionVars = sectionVars_1 ∧
                  sectionFVars = sectionFVars_1 ∧
                    implicitLambda = implicitLambda_1 ∧
                      heedElabAsElim = heedElabAsElim_1 ∧
                        isNoncomputableSection = isNoncomputableSection_1 ∧
                          isMetaSection = isMetaSection_1 ∧
                            ignoreTCFailures = ignoreTCFailures_1 ∧
                              inPattern = inPattern_1 ∧
                                tacSnap? = tacSnap?_1 ∧
                                  saveRecAppSyntax = saveRecAppSyntax_1 ∧
                                    holesAsSyntheticOpaque = holesAsSyntheticOpaque_1 ∧
                                      checkDeprecated = checkDeprecated_1 ∧ fixedTermElabs = fixedTermElabs_1)