proposition: Lemma Nth_app : forall A (l : list A) l' a n, Nth l n a -> Nth (l ++ l') n a.
proof: Proof. Proof using. induction l; intros; simpl in *; try solve_by_inversion. invcs H. - constructor. - constructor. auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)