restrict the scope of macros defined in hlevels.tex to the file
answer Andrej's question
add inference rules from KLV to appendix, without editing them much (yet)