simp only [hasAssignment, hb, ite_true] at h
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment