start updating semanticsExtraTheory, got FV defined

(this used to be called miniMLExtraTheory)