fact: Definition sequence_equality (net : seq_num_network) := forall p p', In p (nwPackets net) -> In p' (nwPackets net) -> (tmNum (pBody p)) = (tmNum (pBody p')) -> pSrc p = pSrc p' -> p = p'.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)