proposition: Theorem ghost_invariant_lower : forall P : _ -> Prop, (forall net net' failed failed' out, step_failure (failed, net) (failed', net') out -> P (deghost net) -> P (deghost net')) -> (forall net net' failed failed' out, @step_failure _ _ failure_params (failed, net) (failed', net') out -> P net -> P net').
proof: Proof. Proof using. intros. apply ghost_simulation_2 with (gnet := reghost net) in H0. - break_exists. intuition. subst. eapply H; eauto. rewrite reghost_deghost_partial_inverses. auto. - eauto using reghost_deghost_partial_inverses. Qed.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)