Kripke semantics for locally namesless values
Identity weakening instead of empty weakening
Type soundness for locally nameless (missing some functoriality and readback)
Removed parameter optimization for Terminates
Removed parameter optimization for Var
Removed parameter optimization for SpineF