fact: Fixpoint processPackets (seq_num : nat) (packets : list (name * msg)) : nat * list (name * seq_num_msg) := match packets with | [] => (seq_num, []) | p :: ps => let (n', pkts) := processPackets seq_num ps in (S n', (fst p, mkseq_num_msg n' (snd p)) :: pkts) end.
imports: Verdi(Verdi)