β-redex comments on Wei Dai’s Shortform