finish writing translation to IL4

untested, unverified

use a trick to avoid having to compute fresh variables or shift de
Bruijn indices: insert NONE for anonymous variables in the list of
variable names used for the translation to de Bruijn, and just keep this
list accurate (i.e. it maintains what would have become shifts).
some termination proofs for IL4

and a pattern-match compilation example evaluation