rcases hi : (insertRatUnits f units).fst.ratUnits[i] with ⟨li, bi⟩
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
⊢ (f.insertRatUnits units).fst.ratUnits[i] ≠ (f.insertRatUnits units).fst.ratUnits[j]
case mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
⊢ (li, bi) ≠ (f.insertRatUnits units).fst.ratUnits[j]