New branch contapprox with alternative definition of evaluation closure

Change Inductive stepn to mstep in Language.v, move stepn back to
CompatibilityUnary.v.
Define new evaluation closure (using mstep), prove new Lemma eval_simpl.