proposition: Theorem ghost_invariant_lift : forall P : _ -> Prop, (forall net net' failed failed' out, @step_failure _ _ failure_params (failed, net) (failed', net') out -> P net -> P net') -> (forall net net' failed failed' out, step_failure (failed, net) (failed', net') out -> P (deghost net) -> P (deghost net')).
proof: Proof. Proof using. intros. eauto using ghost_simulation_1. Qed.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)