{P : Sort u} →
  {root : Aesop.MVarClusterRef} →
    {rootMetaState : Lean.Meta.SavedState} →
      {numGoals numRapps : ℕ} →
        {nextGoalId : Aesop.GoalId} →
          {nextRappId : Aesop.RappId} →
            {allIntroducedMVars : Std.HashSet Lean.MVarId} →
              {root' : Aesop.MVarClusterRef} →
                {rootMetaState' : Lean.Meta.SavedState} →
                  {numGoals' numRapps' : ℕ} →
                    {nextGoalId' : Aesop.GoalId} →
                      {nextRappId' : Aesop.RappId} →
                        {allIntroducedMVars' : Std.HashSet Lean.MVarId} →
                          { root := root, rootMetaState := rootMetaState, numGoals := numGoals, numRapps := numRapps,
                                nextGoalId := nextGoalId, nextRappId := nextRappId,
                                allIntroducedMVars := allIntroducedMVars } =
                              { root := root', rootMetaState := rootMetaState', numGoals := numGoals',
                                numRapps := numRapps', nextGoalId := nextGoalId', nextRappId := nextRappId',
                                allIntroducedMVars := allIntroducedMVars' } →
                            (root = root' →
                                rootMetaState = rootMetaState' →
                                  numGoals = numGoals' →
                                    numRapps = numRapps' →
                                      nextGoalId = nextGoalId' →
                                        nextRappId = nextRappId' → allIntroducedMVars = allIntroducedMVars' → P) →
                              P