fact: Definition sequence_seen (net : seq_num_network) := forall h h' n, In n (assoc_default name_eq_dec (tdSeen (nwState net h')) h []) -> n < (tdNum (nwState net h)).
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)