fact: Record do_network := mkdoNetwork { nwdoPackets : list do_packet ; nwdoState : do_name -> data ; nwdoDisk : do_name -> do_disk file_name }.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)