∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n)
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool)
  (hsize : acc.1.size = n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (i : Fin n),
  acc.1[↑i] = f.assignments[↑i] →
    (∀ l ∈ acc.2.1, ↑l.1 ≠ ↑i) →
      ¬↑l.1 = ↑i →
        have i_lt_assignments_size := ⋯;
        have i_lt_f_assignments_size := ⋯;
        have assignments_i :=
          (acc.1.modify (↑l.1) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment l.2))[↑i];
        have fassignments_i := f.assignments[↑i];
        (assignments_i = fassignments_i ∧ ∀ l_1 ∈ l :: acc.2.1, ¬↑l_1.1 = ↑i) ∨
          (∃ j,
              ↑((l :: acc.2.1).get j).1 = ↑i ∧
                assignments_i =
                    Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment ((l :: acc.2.1).get j).2 fassignments_i ∧
                  ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment ((l :: acc.2.1).get j).2 fassignments_i =
                        true ∧
                    ∀ (k : Fin (l :: acc.2.1).length), ¬k = j → ¬↑((l :: acc.2.1).get k).1 = ↑i) ∨
            ∃ j1 j2,
              ↑((l :: acc.2.1).get j1).1 = ↑i ∧
                ↑((l :: acc.2.1).get j2).1 = ↑i ∧
                  ((l :: acc.2.1).get j1).2 = true ∧
                    ((l :: acc.2.1).get j2).2 = false ∧
                      assignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both ∧
                        fassignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned ∧
                          ∀ (k : Fin (l :: acc.2.1).length), ¬k = j1 → ¬k = j2 → ¬↑((l :: acc.2.1).get k).1 = ↑i