fact: Definition revertLogNetwork (net: log_network) : orig_network := mkNetwork (map revertPacket (nwdoPackets net)) (fun h => (log_data (nwdoState net h))).
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)