proposition: Lemma Nth_tl : forall A (l : list A) a n, Nth l (S n) a -> Nth (List.tl l) n a.
proof: Proof. Proof using. induction l; intros; solve_by_inversion. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)