. apply Nat.le_of_lt_succ
  rw [← Nat.succ_eq_add_one]
  apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j2_ge_idx
  intro idx_eq_j2
  exact idx_ne_j2 (Fin.eq_of_val_eq idx_eq_j2)
case right.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_ne_j2 : ¬idx = j2
⊢ ↑j2 ≥ ↑idx + 1

case right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_ne_j2 : ¬idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    units[j2] = (⟨↑i, ⋯⟩, false) ∧
      (clearUnit assignments units[idx])[↑i] = both ∧
        f.assignments[↑i] = unassigned ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → k ≠ j2 → units[k].fst.val ≠ ↑i
case right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_ne_j2 : ¬idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    units[j2] = (⟨↑i, ⋯⟩, false) ∧
      (clearUnit assignments units[idx])[↑i] = both ∧
        f.assignments[↑i] = unassigned ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → k ≠ j2 → units[k].fst.val ≠ ↑i