. simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
  cases assignment <;> decide
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
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true