simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment).hasNegAssignment = true →
    assignment.hasNegAssignment = true