proved that our partiality type defines a monad.
	modified:   PredicatePart.agda