proposition: Lemma processPackets_nums_unique : forall n l n' l' p p', processPackets n l = (n', l') -> In p l' -> In p' l' -> p <> p' -> (tmNum (snd p)) <> (tmNum (snd p')).
proof: Proof. Proof using. induction l; intros; simpl in *. - invcs H. intuition. - break_match. invcs H. intuition. + subst. intuition. + subst. simpl in *. apply processPackets_correct with (p := p) in Heqp0; intuition auto with zarith. + subst. simpl in *. apply processPackets_correct with (p := p') in Heqp0; intuition auto with zarith. + apply IHl with n0 l0 p p'; auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)