open Preamble

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Lists

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Positive

open Identifiers

type 'a labelled_obj =
  (PreIdentifiers.identifier Types.option, 'a) Types.prod

val instruction_matches_identifier :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  labelled_obj -> Bool.bool

val does_not_occur :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  labelled_obj List.list -> Bool.bool

val occurs_exactly_once :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  labelled_obj List.list -> Bool.bool

val index_of_internal :
  ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> Nat.nat

val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat

val index_of_label :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
  labelled_obj List.list -> Nat.nat