| `Elim of sort (* elimination principle; universe is not relevant *)
| `Projection (* record projection *)
| `InversionPrinciple (* inversion principle *)
+ | `DiscriminationPrinciple (* discrimination principle *)
| `Variant
| `Local
| `Regular ] (* Local = hidden technicality *)