simp only [hasAssignment, hb, ite_false] at h
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.hasNegAssignment = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment