Proved lots of lemmata, wrote minimal_word_of_variables.