I.R15 — Structural Rules Inventory

Inventory of CIC features used by TauLib: inductive types (essential), dependent types (essential), pattern matching (essential), universe polymorphism (cosmetic), Classical.em (2 of 77 modules, eliminable). 74/77 modules fully constructive.