The Kleisli cat on the predicate partiality monad is a rest cat.
	new file:   RestrictionPred.agda