by_cases hb : b
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment

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