proposition: Lemma pt_map_map_pair_eq : forall m m' h failed, pt_map_msg m = Some m' -> Permutation (filterMap pt_map_name_msg (map2snd m (filter_rel adjacent_to_dec h (remove_all name_eq_dec failed nodes)))) (map2snd m' (filter_rel adjacent_to_dec (tot_map_name h) (remove_all name_eq_dec (map tot_map_name failed) nodes))).
proof: Proof. Proof using overlay_map_congr name_map_bijective. move => m m' h failed H_eq. apply pt_nodup_perm_map_map_pair_perm => //; first exact: no_dup_nodes. apply Permutation_sym. exact: permutation_nodes. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)