Expand description
Rocq exporter for the typed LiNo fragment (issue #61).
The exporter intentionally covers the subset that has a direct Rocq counterpart: stratified universes, typed declarations, Pi/lambda/apply, equality expressions, type queries, and simple inductive declarations.