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 **)
let rec identifierTag_rect_Type4 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
| Label -> h_Label
| CostTag -> h_CostTag
| RegisterTag -> h_RegisterTag
| LabelTag -> h_LabelTag
| SymbolTag -> h_SymbolTag
| ASMTag -> h_ASMTag

(** val identifierTag_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
let rec identifierTag_rect_Type5 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
| Label -> h_Label
| CostTag -> h_CostTag
| RegisterTag -> h_RegisterTag
| LabelTag -> h_LabelTag
| SymbolTag -> h_SymbolTag
| ASMTag -> h_ASMTag

(** val identifierTag_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
let rec identifierTag_rect_Type3 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
| Label -> h_Label
| CostTag -> h_CostTag
| RegisterTag -> h_RegisterTag
| LabelTag -> h_LabelTag
| SymbolTag -> h_SymbolTag
| ASMTag -> h_ASMTag

(** val identifierTag_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
let rec identifierTag_rect_Type2 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
| Label -> h_Label
| CostTag -> h_CostTag
| RegisterTag -> h_RegisterTag
| LabelTag -> h_LabelTag
| SymbolTag -> h_SymbolTag
| ASMTag -> h_ASMTag

(** val identifierTag_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
let rec identifierTag_rect_Type1 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
| Label -> h_Label
| CostTag -> h_CostTag
| RegisterTag -> h_RegisterTag
| LabelTag -> h_LabelTag
| SymbolTag -> h_SymbolTag
| ASMTag -> h_ASMTag

(** val identifierTag_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
let rec identifierTag_rect_Type0 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
| Label -> h_Label
| CostTag -> h_CostTag
| RegisterTag -> h_RegisterTag
| LabelTag -> h_LabelTag
| SymbolTag -> h_SymbolTag
| ASMTag -> h_ASMTag

(** val identifierTag_inv_rect_Type4 :
    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let identifierTag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = identifierTag_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val identifierTag_inv_rect_Type3 :
    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let identifierTag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = identifierTag_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val identifierTag_inv_rect_Type2 :
    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let identifierTag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = identifierTag_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val identifierTag_inv_rect_Type1 :
    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let identifierTag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = identifierTag_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val identifierTag_inv_rect_Type0 :
    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let identifierTag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = identifierTag_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val identifierTag_discr : identifierTag -> identifierTag -> __ **)
let identifierTag_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Label -> Obj.magic (fun _ dH -> dH)
     | CostTag -> Obj.magic (fun _ dH -> dH)
     | RegisterTag -> Obj.magic (fun _ dH -> dH)
     | LabelTag -> Obj.magic (fun _ dH -> dH)
     | SymbolTag -> Obj.magic (fun _ dH -> dH)
     | ASMTag -> Obj.magic (fun _ dH -> dH)) y

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

(** val identifier_rect_Type4 :
    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
let rec identifier_rect_Type4 tag h_an_identifier x_2070 =
  let x_2071 = x_2070 in h_an_identifier x_2071

(** val identifier_rect_Type5 :
    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
let rec identifier_rect_Type5 tag h_an_identifier x_2073 =
  let x_2074 = x_2073 in h_an_identifier x_2074

(** val identifier_rect_Type3 :
    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
let rec identifier_rect_Type3 tag h_an_identifier x_2076 =
  let x_2077 = x_2076 in h_an_identifier x_2077

(** val identifier_rect_Type2 :
    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
let rec identifier_rect_Type2 tag h_an_identifier x_2079 =
  let x_2080 = x_2079 in h_an_identifier x_2080

(** val identifier_rect_Type1 :
    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
let rec identifier_rect_Type1 tag h_an_identifier x_2082 =
  let x_2083 = x_2082 in h_an_identifier x_2083

(** val identifier_rect_Type0 :
    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
let rec identifier_rect_Type0 tag h_an_identifier x_2085 =
  let x_2086 = x_2085 in h_an_identifier x_2086

(** val identifier_inv_rect_Type4 :
    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let identifier_inv_rect_Type4 x1 hterm h1 =
  let hcut = identifier_rect_Type4 x1 h1 hterm in hcut __

(** val identifier_inv_rect_Type3 :
    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let identifier_inv_rect_Type3 x1 hterm h1 =
  let hcut = identifier_rect_Type3 x1 h1 hterm in hcut __

(** val identifier_inv_rect_Type2 :
    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let identifier_inv_rect_Type2 x1 hterm h1 =
  let hcut = identifier_rect_Type2 x1 h1 hterm in hcut __

(** val identifier_inv_rect_Type1 :
    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let identifier_inv_rect_Type1 x1 hterm h1 =
  let hcut = identifier_rect_Type1 x1 h1 hterm in hcut __

(** val identifier_inv_rect_Type0 :
    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let identifier_inv_rect_Type0 x1 hterm h1 =
  let hcut = identifier_rect_Type0 x1 h1 hterm in hcut __

(** val identifier_discr :
    identifierTag -> identifier -> identifier -> __ **)
let identifier_discr a1 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y