proposition: Theorem nodup : NoDup Nodes.
proof: Proof. Proof using. unfold Nodes, list_Clients. apply NoDup_cons. - in_crush. discriminate. - apply NoDup_map_injective. + intros. congruence. + apply all_fin_NoDup. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)