proposition: Lemma processPackets_preserves_messages : forall n l, map (fun p => (fst p, tmMsg (snd p))) (snd (processPackets n l)) = l.
proof: Proof. Proof using. induction l. - auto. - simpl. break_match. simpl in *. rewrite IHl. destruct a. auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)