proposition: Lemma lb_step_trace_execution_lb_step_failure_tot_map_net_infseq : forall s, lb_step_execution lb_step_failure s -> lb_step_execution lb_step_failure (map tot_map_net_event s).
proof: Proof. Proof using name_map_bijective multi_map_lb_congr multi_map_congr. cofix c. move => s H_exec. rewrite -tot_map_net_event_map_unfold {1}/tot_map_net_event /=. inversion H_exec; subst => /=. rewrite -tot_map_net_event_map_unfold /= /tot_map_net_event /=. apply: (@Cons_lb_step_exec _ _ _ _ _ _ (List.map tot_map_trace_occ tr)) => /=. - apply: lb_step_failure_tot_mapped_simulation_1. have <-: evt_a e = (fst (evt_a e), snd (evt_a e)) by destruct e, evt_a. by have <-: evt_a e' = (fst (evt_a e'), snd (evt_a e')) by destruct e', evt_a. - simpl in *. find_rewrite. by rewrite map_app. - set e0 := {| evt_a := _ ; evt_l := _ ; evt_trace := _ |}. have ->: e0 = tot_map_net_event e' by []. pose s' := Cons e' s0. rewrite (tot_map_net_event_map_unfold s'). exact: c. Qed.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)