proposition: Lemma In_split_not_In : forall A (p : A) p' xs ys zs, In p (xs ++ p' :: ys) -> ~ In p (zs ++ xs ++ ys) -> p = p'.
proof: Proof. Proof using. intros. find_apply_lem_hyp in_app_iff. simpl in *; intuition; find_false; apply in_app_iff; right; apply in_app_iff; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)