intro heq
case mk.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)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
⊢ (li, bi) ≠ (lj, bj)
case mk.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)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
heq : (li, bi) = (lj, bj)
⊢ False