proposition: Lemma processPackets_seq_eq : forall n l n' l' x y, processPackets n l = (n', l') -> In x l' -> In y l' -> tmNum (snd x) = tmNum (snd y) -> x = y.
proof: Proof. Proof using. induction l; intros; simpl in *. - find_inversion. simpl in *. intuition. - break_match. find_inversion. simpl in *. intuition; subst; simpl in *; eauto; subst; eapply processPackets_correct in Heqp; eauto; lia. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)