by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_of_addNeg, hasNeg_of_addPos]
assignment : Assignment
b : Bool
⊢ hasAssignment b assignment = true ↔ hasAssignment b (addAssignment (decide ¬b = true) assignment) = true
no goals