C.2.3:14.1 - First-pass questions

1. Can a competent reader misread the claim materially? If yes, the expression is likely at F0-F2; if not, it may be F3 or above.
2. Are the critical claims visible as explicit predicates or invariants? If yes, the expression is at least F4.
3. Does the expression have declared executable semantics? If yes, it is likely in the F5-F6 region.
4. Are proofs of the core claims checked by a logic kernel or a dependent type checker? If yes, the expression is likely F7-F8, or F9 if higher-equality machinery is essential.