{P : Sort u} →
  {cache : Lean.Meta.Simp.Cache} →
    {failureCache : Lean.ExprSet} →
      {numSteps : ℕ} →
        {msgLog : List String} →
          {morTheorems transitionTheorems : Mathlib.Meta.FunProp.GeneralTheorems} →
            {cache' : Lean.Meta.Simp.Cache} →
              {failureCache' : Lean.ExprSet} →
                {numSteps' : ℕ} →
                  {msgLog' : List String} →
                    {morTheorems' transitionTheorems' : Mathlib.Meta.FunProp.GeneralTheorems} →
                      { cache := cache, failureCache := failureCache, numSteps := numSteps, msgLog := msgLog,
                            morTheorems := morTheorems, transitionTheorems := transitionTheorems } =
                          { cache := cache', failureCache := failureCache', numSteps := numSteps', msgLog := msgLog',
                            morTheorems := morTheorems', transitionTheorems := transitionTheorems' } →
                        (cache = cache' →
                            failureCache = failureCache' →
                              numSteps = numSteps' →
                                msgLog = msgLog' →
                                  morTheorems = morTheorems' → transitionTheorems = transitionTheorems' → P) →
                          P