. simp only [Bool.not_eq_true] at hb
  simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
  cases assignment <;> decide
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
no goals