proposition: Lemma revertNetwork_packets : forall xs net (p : seq_num_packet) ys, ~ In (tmNum (pBody p)) (assoc_default name_eq_dec (tdSeen (nwState net (pDst p))) (pSrc p) []) -> nwPackets net = xs ++ p :: ys -> exists xs' ys', nwPackets (revertNetwork net) = xs' ++ (revertPacket p) :: ys'.
proof: Proof. Proof using. intros. apply in_split. apply revertNetwork_In; repeat find_rewrite; intuition auto with datatypes. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)