example (α : Sort u) : Subsingleton (Squash α) := inferInstance