minor cleanup, and a new lemma

term_union_insert_append was a generalisation of term_union_sing_lt.
rename it to term_union_insert and also add term_union_replace.