have h := not_hasPos_of_removePos assignment
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.removePosAssignment.hasPosAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true