Upstream Primitive Projections

As the equivalent of "carbon offsets", we can add more Primitive Projections to Iris to make proofs faster. An MR for this issue is currently ongoing here.