it's not as bad, exp_preserves_sub_pr doesn't need oktrans2notrans, but it it needs precise substitution+narrowing