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_update_auth_persist to 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)).
Cc #439