Prohibiting invalid states with GADT - the airlock exercise

Would someone like to show how to replace the pipe here with let*? Would that make sense?