Skip to content
GitLab

rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)

Merged Ralf Jung requested to merge ralf/map_union_subseteq into master

This is more consistent with or_intro_{l,r}' and !300 (merged).

Merge request reports