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. :)

Also I was not sure what to call this. I considered dom_insert_elem_of as alternative, but there is no ∈ in the lemma statement, so that seems odd.

Also I was not sure what to call this. I considered dom_insert_elem_of as alternative, but there is no ∈ in the lemma statement, so that seems odd.

The name in this MR makes sense.

resolved all threads

added 1 commit

• 5514ae41 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

merged

mentioned in commit ef15fdb9

Merged. Thanks.