eta expand translations of receive and wait
convoluted transformation of receive that seems to allow the proof to
go through