proposition: Theorem In_n_Nodes : forall n : Name, In n Nodes.
proof: Proof. Proof using. intros. unfold Nodes, list_Clients. simpl. destruct n. - right. apply in_map. apply all_fin_all. - left. reflexivity. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)