is mentioned by

Thm* x,y:. |x| = |y| x = y

[absval_eq]

Try larger context: StandardLIB