proposition: Theorem mgv_ghost_simulation_2 : forall net net' failed failed' out gnet, @step_failure _ _ failure_params (failed, net) (failed', net') out -> mgv_deghost gnet = net -> exists gnet', step_failure (failed, gnet) (failed', gnet') out /\ mgv_deghost gnet' = net'.
proof: Proof. Proof using. move => net net' failed failed' out gnet H_step H_eq. eapply step_failure_tot_mapped_simulation_2 in H_step => //. - move: H_step => [gnet' [H_step H_eq_net]]. exists gnet'. split; eauto. rewrite -H_eq_net {H_step H_eq_net}. rewrite /mgv_deghost /tot_map_net /= /id /= /tot_map_packet /= /id /=. set nwPf1 := fun p : packet => _. set nwPf2 := fun p : packet => _. have H_eq_p: nwPf1 = nwPf2 by rewrite /nwPf1 /nwPf2 {nwPf1 nwPf2}; apply functional_extensionality; case. set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2 by rewrite /nwS1 /nwS2 {nwS1 nwS2}; apply functional_extensionality => n; case: gnet'. by rewrite H_eq_p H_eq_s. - rewrite -H_eq {H_step H_eq}. rewrite /mgv_deghost /tot_map_net /= /id /= /tot_map_packet /= /id /=. set nwPf1 := fun p : packet => _. set nwPf2 := fun p : packet => _. have H_eq_p: nwPf1 = nwPf2 by rewrite /nwPf1 /nwPf2 {nwPf1 nwPf2}; apply functional_extensionality; case. set nwS1 := fun _ => _. set nwS2 := fun _ => _. have H_eq_s: nwS1 = nwS2 by rewrite /nwS1 /nwS2 {nwS1 nwS2}; apply functional_extensionality => n; case: gnet. by rewrite H_eq_p H_eq_s. - by rewrite /tot_map_name /= map_id. - by rewrite /tot_map_name /= map_id. - move {H_step}. elim: out => //. case => n t out IH. case: t => /=; first by move => inp; rewrite /id /= IH. move => out'. by rewrite {1}/id map_id /= IH. Qed.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)