proposition: Lemma Nth_snoc : forall A (l : list A) x, Nth (l ++ [x]) (length l) x.
proof: Proof. Proof using. intros. induction l; simpl in *; constructor; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)