-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.mk.inj : ∀ {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