minor progress with (nen≤ α <$> nereadback t) ~ nereadback (nev≤ α t)

	modified:   SpinelessValues.agda