There are some proof rules on ℙ that could also work on ℙ1, but are not implemented.
For example, finite(ℙ(0‥n)) is proved automatically, but finite(ℙ1(0‥n)) is not.
We should review all the proof rules on ℙ and implement them for ℙ1 when applicable.
After reviewing all proof rules on ℙ, it appears that two rules are missing for ℙ1:
These rules will be added whenever we create a new level of the auto rewriter.