by_cases hb : b
assignment : Assignment
b : Bool
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true