simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
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
⊢ f.assignments[↑i] = f.assignments[↑i] ∧ ∀ (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), ¬f.ratUnits[↑j].fst.val = ↑i