∀ {eAssignment : Array (Option Lean.Expr)} {uAssignment : Array (Option Lean.Level)}
  {ePending : Array (Lean.Expr × Lean.Expr)} {uPending : Array (Lean.Level × Lean.Level)}
  {iPending : Array (Lean.Expr × Lean.Expr)} {tPending : Array ℕ} {us : List Lean.Level} {args : Array Lean.Expr}
  {eAssignment_1 : Array (Option Lean.Expr)} {uAssignment_1 : Array (Option Lean.Level)}
  {ePending_1 : Array (Lean.Expr × Lean.Expr)} {uPending_1 : Array (Lean.Level × Lean.Level)}
  {iPending_1 : Array (Lean.Expr × Lean.Expr)} {tPending_1 : Array ℕ} {us_1 : List Lean.Level}
  {args_1 : Array Lean.Expr},
  { eAssignment := eAssignment, uAssignment := uAssignment, ePending := ePending, uPending := uPending,
        iPending := iPending, tPending := tPending, us := us, args := args } =
      { eAssignment := eAssignment_1, uAssignment := uAssignment_1, ePending := ePending_1, uPending := uPending_1,
        iPending := iPending_1, tPending := tPending_1, us := us_1, args := args_1 } →
    eAssignment = eAssignment_1 ∧
      uAssignment = uAssignment_1 ∧
        ePending = ePending_1 ∧
          uPending = uPending_1 ∧ iPending = iPending_1 ∧ tPending = tPending_1 ∧ us = us_1 ∧ args = args_1