∀ {numVarsSucc : ℕ} {clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc))}
  {rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))}
  {assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment}
  {clauses_1 : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc))}
  {rupUnits_1 ratUnits_1 : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))}
  {assignments_1 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment},
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =
      { clauses := clauses_1, rupUnits := rupUnits_1, ratUnits := ratUnits_1, assignments := assignments_1 } →
    clauses = clauses_1 ∧ rupUnits = rupUnits_1 ∧ ratUnits = ratUnits_1 ∧ assignments = assignments_1