fact: Definition deghost_packet p := @mkPacket _ multi_params (@pSrc _ refined_multi_params p) (pDst p) (pBody p).
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)