add labels to predicates but no change to proof
fix BitsUnchanged and use it in various specs