simp only [hf.1, Array.size_toArray, List.length_nil] at j
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j : Fin f.ratUnits.size
⊢ ¬f.ratUnits[↑j].fst.val = ↑i
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j✝ : Fin f.ratUnits.size
j : Fin 0
⊢ ¬f.ratUnits[↑j✝].fst.val = ↑i