add insert_subseteq_l

Merged Ralf Jung requested to merge ralf/insert_subseteq_l into master

A useful little lemma to iteratively build up map inclusion (just needed this in Perennial).

Merge request reports