∀ {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_1 : ℕ}
  {proc_1 : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))}
  {suspend_1 : Lean.MVarId → Lean.MetaM Bool} {discharge_1 : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))}
  {commitIndependentGoals_1 : Bool},
  { maxDepth := maxDepth, proc := proc, suspend := suspend, discharge := discharge,
        commitIndependentGoals := commitIndependentGoals } =
      { maxDepth := maxDepth_1, proc := proc_1, suspend := suspend_1, discharge := discharge_1,
        commitIndependentGoals := commitIndependentGoals_1 } →
    maxDepth = maxDepth_1 ∧
      proc = proc_1 ∧ suspend = suspend_1 ∧ discharge = discharge_1 ∧ commitIndependentGoals = commitIndependentGoals_1