rw [addAssignment, hasAssignment]
assignment : Assignment
b : Bool
⊢ hasAssignment b (addAssignment b assignment) = true
assignment : Assignment
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment)
      ((if b = true then addPosAssignment else addNegAssignment) assignment) =
    true