. simp only [clearUnit, Fin.getElem_fin, Array.get_eq_getElem]
  specialize ih2 idx (Nat.le_refl idx.val)
  have idx_unit_in_bounds : units[idx].1.1 < assignments.size := by
    rw [hsize]; exact units[idx].1.2.2
  have i_in_bounds : i.1 < assignments.size := by
    rw [hsize]
    exact i.2
  have h := Array.get_modify_unchanged idx_unit_in_bounds i_in_bounds (removeAssignment units[idx.val].2) ih2
  simp only [Fin.getElem_fin] at h
  rw [h]
  exact ih1
case intro.inl.intro.h.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
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
⊢ (clearUnit assignments units[idx])[↑i] = f.assignments[↑i]

case intro.inl.intro.h.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
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
⊢ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i
case intro.inl.intro.h.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
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
⊢ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i