fact: Definition do_send_packets src ps := (map (fun m => mklPacket src (fst m) (snd m)) ps).
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)