@mflatt is right: no need for the freshness constraint before beta-reducing... it does not hurt, though