open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Positive

type identifierTag =
| Label
| CostTag
| RegisterTag
| LabelTag
| SymbolTag
| ASMTag

val identifierTag_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1

val identifierTag_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1

val identifierTag_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1

val identifierTag_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1

val identifierTag_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1

val identifierTag_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1

val identifierTag_inv_rect_Type4 :
  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val identifierTag_inv_rect_Type3 :
  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val identifierTag_inv_rect_Type2 :
  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val identifierTag_inv_rect_Type1 :
  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val identifierTag_inv_rect_Type0 :
  identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val identifierTag_discr : identifierTag -> identifierTag -> __

type identifier =
  Positive.pos
  (* singleton inductive, whose constructor was an_identifier *)

val identifier_rect_Type4 :
  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1

val identifier_rect_Type5 :
  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1

val identifier_rect_Type3 :
  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1

val identifier_rect_Type2 :
  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1

val identifier_rect_Type1 :
  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1

val identifier_rect_Type0 :
  identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1

val identifier_inv_rect_Type4 :
  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1

val identifier_inv_rect_Type3 :
  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1

val identifier_inv_rect_Type2 :
  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1

val identifier_inv_rect_Type1 :
  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1

val identifier_inv_rect_Type0 :
  identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1

val identifier_discr : identifierTag -> identifier -> identifier -> __