Before revision:  This gives an easy proof of ER-membership, as real verification algorithms are much more versatile than ETR-formulas  .
After revision:  This gives an easy proof of ER-membership, as verification algorithms on a real RAM are much more versatile than ETR-formulas .