exact Fin.elim0 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
j : Fin 0
⊢ ¬f.ratUnits[↑j✝].fst.val = ↑i
no goals