{P : Sort u} →
  {maxDepth : ℕ} →
    {proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))} →
      {suspend : Lean.MVarId → Lean.MetaM Bool} →
        {discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))} →
          {commitIndependentGoals : Bool} →
            {maxDepth' : ℕ} →
              {proc' : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))} →
                {suspend' : Lean.MVarId → Lean.MetaM Bool} →
                  {discharge' : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))} →
                    {commitIndependentGoals' : Bool} →
                      { maxDepth := maxDepth, proc := proc, suspend := suspend, discharge := discharge,
                            commitIndependentGoals := commitIndependentGoals } =
                          { maxDepth := maxDepth', proc := proc', suspend := suspend', discharge := discharge',
                            commitIndependentGoals := commitIndependentGoals' } →
                        (maxDepth = maxDepth' →
                            proc = proc' →
                              suspend = suspend' →
                                discharge = discharge' → commitIndependentGoals = commitIndependentGoals' → P) →
                          P