rcases hi : (insertRupUnits f units).fst.rupUnits[i] with ⟨li, bi⟩
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
⊢ (f.insertRupUnits units).fst.rupUnits[i] ≠ (f.insertRupUnits units).fst.rupUnits[j]
case mk
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
⊢ (li, bi) ≠ (f.insertRupUnits units).fst.rupUnits[j]