Almost proved commutativity of the first triangle for product in the Delay monad
	modified:   RestrictionDelay.agda