proposition: Theorem mgv_ghost_simulation_1 : forall net net' failed failed' out, @step_failure _ _ mgv_refined_failure_params (failed, net) (failed', net') out -> @step_failure _ _ failure_params (failed, mgv_deghost net) (failed', mgv_deghost net') out.
proof: Proof. Proof using. move => net net' failed failed' out H_step. apply step_failure_tot_mapped_simulation_1 in H_step. rewrite /tot_map_name /tot_map_net /= 2!map_id /id /= in H_step. rewrite /tot_map_trace_occ /= /id /= in H_step. rewrite /tot_map_packet /= /id /= in H_step. rewrite /mgv_deghost /=. rewrite -/id mgv_map_id_tr in H_step. move: H_step. set fp := fun p : packet => _. set fp' := fun p : packet => _. have H_eq: fp = fp' by rewrite /fp /fp'; apply functional_extensionality; case => /= src dst m. rewrite H_eq {H_eq fp}. set fs1 := fun n => _. set fs2 := fun n => _. set fs1' := fun n => _. set fs2' := fun n => _. have H_eq: fs1 = fs1' by rewrite /fs1 /fs1' {fs1 fs1'}; apply functional_extensionality => n; case: net. rewrite H_eq {H_eq fs1}. have H_eq: fs2 = fs2' by rewrite /fs2 /fs2' {fs2 fs2'}; apply functional_extensionality => n; case: net'. by rewrite H_eq. Qed.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)