{motive : Lean.Elab.Term.Context → Sort u} →
  (t : Lean.Elab.Term.Context) →
    ((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 ignoreTCFailures inPattern : Bool) →
                      (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        (saveRecAppSyntax holesAsSyntheticOpaque checkDeprecated : Bool) →
                          (fixedTermElabs : Array Lean.Elab.Term.FixedTermElabRef) →
                            motive
                              { declName? := declName?, macroStack := macroStack, mayPostpone := mayPostpone,
                                errToSorry := errToSorry, autoBoundImplicitContext := autoBoundImplicitContext,
                                autoBoundImplicitForbidden := autoBoundImplicitForbidden, sectionVars := sectionVars,
                                sectionFVars := sectionFVars, implicitLambda := implicitLambda,
                                heedElabAsElim := heedElabAsElim, isNoncomputableSection := isNoncomputableSection,
                                ignoreTCFailures := ignoreTCFailures, inPattern := inPattern, tacSnap? := tacSnap?,
                                saveRecAppSyntax := saveRecAppSyntax, holesAsSyntheticOpaque := holesAsSyntheticOpaque,
                                checkDeprecated := checkDeprecated, fixedTermElabs := fixedTermElabs }) →
      motive t