| `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 *)
method virtual ppterm: context:context -> subst:substitution ->
metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
method virtual ppterm: context:context -> subst:substitution ->
metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string