proposition: Lemma map_map_pair_eq : forall h m failed, Permutation (map (fun nm : name * msg => (tot_map_name (fst nm), tot_map_msg (snd nm))) (map2snd m (filter_rel adjacent_to_dec h (remove_all name_eq_dec failed nodes)))) (map2snd (tot_map_msg 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 => h m failed. apply nodup_perm_map_map_pair_perm; first exact: no_dup_nodes. apply Permutation_sym. exact: permutation_nodes. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)