open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

type order =
| Order_lt
| Order_eq
| Order_gt

(** val order_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
let rec order_rect_Type4 h_order_lt h_order_eq h_order_gt = function
| Order_lt -> h_order_lt
| Order_eq -> h_order_eq
| Order_gt -> h_order_gt

(** val order_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
let rec order_rect_Type5 h_order_lt h_order_eq h_order_gt = function
| Order_lt -> h_order_lt
| Order_eq -> h_order_eq
| Order_gt -> h_order_gt

(** val order_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
let rec order_rect_Type3 h_order_lt h_order_eq h_order_gt = function
| Order_lt -> h_order_lt
| Order_eq -> h_order_eq
| Order_gt -> h_order_gt

(** val order_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
let rec order_rect_Type2 h_order_lt h_order_eq h_order_gt = function
| Order_lt -> h_order_lt
| Order_eq -> h_order_eq
| Order_gt -> h_order_gt

(** val order_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
let rec order_rect_Type1 h_order_lt h_order_eq h_order_gt = function
| Order_lt -> h_order_lt
| Order_eq -> h_order_eq
| Order_gt -> h_order_gt

(** val order_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
let rec order_rect_Type0 h_order_lt h_order_eq h_order_gt = function
| Order_lt -> h_order_lt
| Order_eq -> h_order_eq
| Order_gt -> h_order_gt

(** val order_inv_rect_Type4 :
    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let order_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = order_rect_Type4 h1 h2 h3 hterm in hcut __

(** val order_inv_rect_Type3 :
    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let order_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = order_rect_Type3 h1 h2 h3 hterm in hcut __

(** val order_inv_rect_Type2 :
    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let order_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = order_rect_Type2 h1 h2 h3 hterm in hcut __

(** val order_inv_rect_Type1 :
    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let order_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = order_rect_Type1 h1 h2 h3 hterm in hcut __

(** val order_inv_rect_Type0 :
    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let order_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = order_rect_Type0 h1 h2 h3 hterm in hcut __

(** val order_discr : order -> order -> __ **)
let order_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Order_lt -> Obj.magic (fun _ dH -> dH)
     | Order_eq -> Obj.magic (fun _ dH -> dH)
     | Order_gt -> Obj.magic (fun _ dH -> dH)) y