Some functoriality proofs (closing gaps in LocallyNamelessValues)
Functoriality for lev-le.  lookupLev-le needs heterogeneous equality
Stuck with het.eq