formaltex: Pi-intro was simplified, so simplify the sample derivation correspondingly