have h := not_hasNeg_of_removeNeg assignment
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.removeNegAssignment.hasNegAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true