change SPred to be "bounded": they must hold a step-index 0. Change SPred-n-equality to require equivalence even at level n.

This gives rise to a nice lemma relation validity at level n, and n-equality. Plus, it works nicely for all existing constructions in lib/ (mainly because equality was already bounded)