removed R2 postulate
	modified:   RestrictionDelay.agda