rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
⊢ (f.assignments.modify l.val addPosAssignment).size = n
no goals