open Preamble

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

open Proper

open Div_and_mod

open Util

open Extralib

open IOMonad

type monadFunctRel =
| Mk_MonadFunctRel

(** val monadFunctRel_rect_Type4 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel -> 'a1 **)
let rec monadFunctRel_rect_Type4 m1 m2 h_mk_MonadFunctRel = function
| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __

(** val monadFunctRel_rect_Type5 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel -> 'a1 **)
let rec monadFunctRel_rect_Type5 m1 m2 h_mk_MonadFunctRel = function
| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __

(** val monadFunctRel_rect_Type3 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel -> 'a1 **)
let rec monadFunctRel_rect_Type3 m1 m2 h_mk_MonadFunctRel = function
| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __

(** val monadFunctRel_rect_Type2 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel -> 'a1 **)
let rec monadFunctRel_rect_Type2 m1 m2 h_mk_MonadFunctRel = function
| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __

(** val monadFunctRel_rect_Type1 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel -> 'a1 **)
let rec monadFunctRel_rect_Type1 m1 m2 h_mk_MonadFunctRel = function
| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __

(** val monadFunctRel_rect_Type0 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel -> 'a1 **)
let rec monadFunctRel_rect_Type0 m1 m2 h_mk_MonadFunctRel = function
| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __

(** val monadFunctRel_inv_rect_Type4 :
    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let monadFunctRel_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = monadFunctRel_rect_Type4 x1 x2 h1 hterm in hcut __

(** val monadFunctRel_inv_rect_Type3 :
    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let monadFunctRel_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = monadFunctRel_rect_Type3 x1 x2 h1 hterm in hcut __

(** val monadFunctRel_inv_rect_Type2 :
    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let monadFunctRel_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = monadFunctRel_rect_Type2 x1 x2 h1 hterm in hcut __

(** val monadFunctRel_inv_rect_Type1 :
    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let monadFunctRel_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = monadFunctRel_rect_Type1 x1 x2 h1 hterm in hcut __

(** val monadFunctRel_inv_rect_Type0 :
    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let monadFunctRel_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = monadFunctRel_rect_Type0 x1 x2 h1 hterm in hcut __

(** val monadFunctRel_jmdiscr :
    Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __ **)
let monadFunctRel_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (let Mk_MonadFunctRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y

type monadFunctRel1 =
| Mk_MonadFunctRel1

(** val monadFunctRel1_rect_Type4 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel1 -> 'a1 **)
let rec monadFunctRel1_rect_Type4 m1 m2 h_mk_MonadFunctRel1 = function
| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __

(** val monadFunctRel1_rect_Type5 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel1 -> 'a1 **)
let rec monadFunctRel1_rect_Type5 m1 m2 h_mk_MonadFunctRel1 = function
| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __

(** val monadFunctRel1_rect_Type3 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel1 -> 'a1 **)
let rec monadFunctRel1_rect_Type3 m1 m2 h_mk_MonadFunctRel1 = function
| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __

(** val monadFunctRel1_rect_Type2 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel1 -> 'a1 **)
let rec monadFunctRel1_rect_Type2 m1 m2 h_mk_MonadFunctRel1 = function
| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __

(** val monadFunctRel1_rect_Type1 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel1 -> 'a1 **)
let rec monadFunctRel1_rect_Type1 m1 m2 h_mk_MonadFunctRel1 = function
| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __

(** val monadFunctRel1_rect_Type0 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadFunctRel1 -> 'a1 **)
let rec monadFunctRel1_rect_Type0 m1 m2 h_mk_MonadFunctRel1 = function
| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __

(** val monadFunctRel1_inv_rect_Type4 :
    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
    __ -> __ -> 'a1) -> 'a1 **)
let monadFunctRel1_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = monadFunctRel1_rect_Type4 x1 x2 h1 hterm in hcut __

(** val monadFunctRel1_inv_rect_Type3 :
    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
    __ -> __ -> 'a1) -> 'a1 **)
let monadFunctRel1_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = monadFunctRel1_rect_Type3 x1 x2 h1 hterm in hcut __

(** val monadFunctRel1_inv_rect_Type2 :
    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
    __ -> __ -> 'a1) -> 'a1 **)
let monadFunctRel1_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = monadFunctRel1_rect_Type2 x1 x2 h1 hterm in hcut __

(** val monadFunctRel1_inv_rect_Type1 :
    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
    __ -> __ -> 'a1) -> 'a1 **)
let monadFunctRel1_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = monadFunctRel1_rect_Type1 x1 x2 h1 hterm in hcut __

(** val monadFunctRel1_inv_rect_Type0 :
    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
    __ -> __ -> 'a1) -> 'a1 **)
let monadFunctRel1_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = monadFunctRel1_rect_Type0 x1 x2 h1 hterm in hcut __

(** val monadFunctRel1_jmdiscr :
    Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __ **)
let monadFunctRel1_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (let Mk_MonadFunctRel1 = x in Obj.magic (fun _ dH -> dH __ __ __ __ __))
    y

type monadGenRel =
| Mk_MonadGenRel

(** val monadGenRel_rect_Type4 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadGenRel -> 'a1 **)
let rec monadGenRel_rect_Type4 m1 m2 h_mk_MonadGenRel = function
| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __

(** val monadGenRel_rect_Type5 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadGenRel -> 'a1 **)
let rec monadGenRel_rect_Type5 m1 m2 h_mk_MonadGenRel = function
| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __

(** val monadGenRel_rect_Type3 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadGenRel -> 'a1 **)
let rec monadGenRel_rect_Type3 m1 m2 h_mk_MonadGenRel = function
| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __

(** val monadGenRel_rect_Type2 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadGenRel -> 'a1 **)
let rec monadGenRel_rect_Type2 m1 m2 h_mk_MonadGenRel = function
| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __

(** val monadGenRel_rect_Type1 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadGenRel -> 'a1 **)
let rec monadGenRel_rect_Type1 m1 m2 h_mk_MonadGenRel = function
| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __

(** val monadGenRel_rect_Type0 :
    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
    monadGenRel -> 'a1 **)
let rec monadGenRel_rect_Type0 m1 m2 h_mk_MonadGenRel = function
| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __

(** val monadGenRel_inv_rect_Type4 :
    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let monadGenRel_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = monadGenRel_rect_Type4 x1 x2 h1 hterm in hcut __

(** val monadGenRel_inv_rect_Type3 :
    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let monadGenRel_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = monadGenRel_rect_Type3 x1 x2 h1 hterm in hcut __

(** val monadGenRel_inv_rect_Type2 :
    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let monadGenRel_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = monadGenRel_rect_Type2 x1 x2 h1 hterm in hcut __

(** val monadGenRel_inv_rect_Type1 :
    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let monadGenRel_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = monadGenRel_rect_Type1 x1 x2 h1 hterm in hcut __

(** val monadGenRel_inv_rect_Type0 :
    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let monadGenRel_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = monadGenRel_rect_Type0 x1 x2 h1 hterm in hcut __

(** val monadGenRel_jmdiscr :
    Monad.monad -> Monad.monad -> monadGenRel -> monadGenRel -> __ **)
let monadGenRel_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (let Mk_MonadGenRel = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y

(** val res_preserve : monadFunctRel **)
let res_preserve =
  Mk_MonadFunctRel

(** val res_preserve1 : monadFunctRel1 **)
let res_preserve1 =
  Mk_MonadFunctRel1

(** val gen_res_preserve : monadGenRel **)
let gen_res_preserve =
  Mk_MonadGenRel

(** val opt_preserve : monadFunctRel **)
let opt_preserve =
  Mk_MonadFunctRel

(** val opt_preserve1 : monadFunctRel1 **)
let opt_preserve1 =
  Mk_MonadFunctRel1

(** val gen_opt_preserve : monadGenRel **)
let gen_opt_preserve =
  Mk_MonadGenRel

(** val io_preserve : monadFunctRel **)
let io_preserve =
  Mk_MonadFunctRel

(** val io_preserve1 : monadFunctRel1 **)
let io_preserve1 =
  Mk_MonadFunctRel1

(** val gen_io_preserve : monadGenRel **)
let gen_io_preserve =
  Mk_MonadGenRel