defn of closed that takes shorts and longs into account

so values are closed wrt a module env as opposed to without context.
proved evaluate_closed
get semanticsExtraTheory to build