add dom_insert_lookup

I was just looking for this lemma and couldn't find it, so I figured it might be good to add. :)