proposition: Lemma revertNetwork_In : forall net (p : seq_num_packet), In p (nwPackets net) -> ~ In (tmNum (pBody p)) (assoc_default name_eq_dec (tdSeen (nwState net (pDst p))) (pSrc p) []) -> In (revertPacket p) (nwPackets (revertNetwork net)).
proof: Proof. Proof using. intros. unfold revertNetwork. simpl in *. in_crush. apply filter_In. intuition. - apply dedup_In. auto. - break_if; intuition. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)