proposition: Lemma processPackets_dedup : forall processed (rest : list seq_num_packet) n' l h net, (forall p, In p rest -> In p (nwPackets net)) -> sequence_sane net -> processPackets (tdNum (nwState net h)) l = (n', processed) -> dedup pkt_eq_dec ((@send_packets _ multi_params h processed) ++ rest) = (send_packets h processed) ++ (dedup pkt_eq_dec rest).
proof: Proof. Proof using. intros. simpl in *. rewrite dedup_app; f_equal. - apply dedup_NoDup_id. apply NoDup_map_injective; eauto using processPackets_NoDup. intros. find_inversion. rewrite surjective_pairing at 1. rewrite surjective_pairing. unfold msg in *. simpl in *. repeat find_rewrite. auto. - intuition. subst. find_apply_lem_hyp in_map_iff. break_exists. intuition. find_eapply_lem_hyp processPackets_ge_start; eauto. match goal with | _ : In ?p _, net : network |- _ => assert (In p (nwPackets net)) by eauto end. unfold sequence_sane in *. find_apply_hyp_hyp. simpl in *. subst. simpl in *. lia. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)