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

val order_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1

val order_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1

val order_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1

val order_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1

val order_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1

val order_inv_rect_Type4 :
  order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val order_inv_rect_Type3 :
  order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val order_inv_rect_Type2 :
  order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val order_inv_rect_Type1 :
  order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val order_inv_rect_Type0 :
  order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val order_discr : order -> order -> __