proposition: Lemma Nth_something_at_head : forall A (l : list A) n x, Nth l n x -> exists y l', l = y :: l'.
proof: Proof. Proof using. intros. solve_by_inversion' eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)