fact: Definition deghost_prop I (failed_net : list name * network) : Prop := I ((fst failed_net), deghost (snd failed_net)).
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)