proposition: Lemma processPackets_NoDup : forall n l n' l', processPackets n l = (n', l') -> NoDup l'.
proof: Proof. Proof using. induction l; intros. - simpl in *. find_inversion. constructor. - simpl in *. break_match. find_inversion. specialize (IHl n0 l0). concludes. constructor; auto. intro. eapply processPackets_correct in H; eauto. simpl in *. lia. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)