proposition: Lemma step_ordered_dynamic_failure_tot_one_mapped_simulation_1_init : forall net net' failed failed' tr, step_ordered_dynamic_failure (failed, net) (failed', net') tr -> net.(odnwState) me = None -> forall d, net'.(odnwState) me = Some d -> tot_s_map_data d = init_handler.
proof: Proof. Proof using map_congr. move => net net' failed failed' tr H_st H_eq d H_eq'. invcs H_st => //=. - move: H_eq'. rewrite /update. break_if => H_eq'; last by congruence. find_injection. by rewrite tot_s_init_handlers_eq. - move: H_eq'. rewrite /update. by break_if => H_eq'; congruence. - move: H_eq'. rewrite /update. by break_if => H_eq'; congruence. - by congruence. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(Ssrexport)