ch:logic-enriched-type-theory: proposition classification
Problem and invariant. Decide which of three quantifier levels is admissible for small comprehension, small formula implies analytic formula.
Two representations. A maximum-quantifier-level integer is compact; the selected recursive syntax tree keeps implication branches and every rejection visible.
First complete version. Define the three sorts and formula tree. Implement small first, add analytic, then wire the three operations to those decisions. Add the implication guard before printing.
Observable result. Five named cases pass and the final line is All 5 Chapter 92 corpus cases passed.
A failing version. Make comprehension call analytic. The set-quantifier rejection changes to FAIL; the inline test exits 1.
Acceptance and boundary. Run the check/test/run/audit commands in subappendix E.7, require exact stdout and [], restore the mutation, and repeat. The program classifies finite syntax; it does not prove LTT conservativity.