given
postulate nereadback≤ : ∀{Γ Δ a}(α : Δ ≤ Γ)(t : Ne Val Γ a){n : Ne Nf Γ a} →
              nereadback t ⇓ n → nereadback (nev≤ α t) ⇓ nen≤ α n

I can prove rterm/rterm'
	modified:   Delay.agda
	modified:   SpinelessValues.agda