replace my "squash" by Notation squash := ishinh_UU.