| `Elim of sort (* elimination principle; universe is not relevant *)
| `Projection (* record projection *)
| `InversionPrinciple (* inversion principle *)
| `Elim of sort (* elimination principle; universe is not relevant *)
| `Projection (* record projection *)
| `InversionPrinciple (* inversion principle *)