proposition: Lemma remove_tot_map_eq : forall h failed, map tot_map_name (remove name_eq_dec h failed) = remove name_eq_dec (tot_map_name h) (map tot_map_name failed).
proof: Proof. Proof using name_map_bijective. move => h. elim => //=. move => n failed IH. repeat break_if => //. - by find_rewrite. - by find_apply_lem_hyp tot_map_name_injective. - by rewrite /= IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)