simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i