changes in value definitions, add tm_lvl and values_are_terms lemma, reformulate progress theorem