I went over the lemmas in this file and they all looked reasonable. The notation already follows the proposal in #412. The only change I made is to rename
mono_list_auth_persist. "persist" always requires an update, and this is consistent with
gmap_view_auth_persist (already in master, though fairly recently) and
mono_nat_auth_persist (to be added in !759 (merged)).