Sized convergence
	modified:   Delay.agda