{motive : Lean.Meta.Context → Sort u} →
  (t : Lean.Meta.Context) →
    ((keyedConfig : Lean.Meta.ConfigWithKey) →
        (trackZetaDelta : Bool) →
          (zetaDeltaSet : Lean.FVarIdSet) →
            (lctx : Lean.LocalContext) →
              (localInstances : Lean.LocalInstances) →
                (defEqCtx? : Option Lean.Meta.DefEqContext) →
                  (synthPendingDepth : ℕ) →
                    (canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool)) →
                      (univApprox inTypeClassResolution cacheInferType : Bool) →
                        motive
                          { keyedConfig := keyedConfig, trackZetaDelta := trackZetaDelta, zetaDeltaSet := zetaDeltaSet,
                            lctx := lctx, localInstances := localInstances, defEqCtx? := defEqCtx?,
                            synthPendingDepth := synthPendingDepth, canUnfold? := canUnfold?, univApprox := univApprox,
                            inTypeClassResolution := inTypeClassResolution, cacheInferType := cacheInferType }) →
      motive t