contradiction
case mk.mk.refl.inl.intro
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)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ¬(li, bi).fst.val = li.val
⊢ False
no goals