More uniform processing, at the cost of the encoding of 'restrict'
and 'extend' and not processing K_props and identity_props (they use
S_pred things).

surjective pairing
projections