isn't this relying on properties that aren't proven about pi? it needs to be disjunctive or normal, and neither of those are proven