simp only [unit, hc]
case clause
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hc : c.clause = [(i, b)]
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_eq_c : (i, b) = (l, false)
⊢ (unit (i, b)).clause = c.clause
no goals