fact: Definition do_packet_eq_dec (p q : do_packet) : {p = q} + {p <> q}.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)