. simp only [removeAssignment, hb, addAssignment, ite_true]
  simp only [hasAssignment, hb, ite_false] at h
  exact removeNeg_addNeg_cancel h
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
no goals