introduce the "semi-intrinsic" encoding of theorems and rules:
    add LF_Empty type
    add an LF axiom "WildCard : LF_Empty"
    make all the definitions in semi-intrinsic.ts work, just as in judged_expressions.ts