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

val monadFunctRel_rect_Type5 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel -> 'a1

val monadFunctRel_rect_Type3 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel -> 'a1

val monadFunctRel_rect_Type2 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel -> 'a1

val monadFunctRel_rect_Type1 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel -> 'a1

val monadFunctRel_rect_Type0 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel -> 'a1

val monadFunctRel_inv_rect_Type4 :
  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
  -> 'a1) -> 'a1

val monadFunctRel_inv_rect_Type3 :
  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
  -> 'a1) -> 'a1

val monadFunctRel_inv_rect_Type2 :
  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
  -> 'a1) -> 'a1

val monadFunctRel_inv_rect_Type1 :
  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
  -> 'a1) -> 'a1

val monadFunctRel_inv_rect_Type0 :
  Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ -> __
  -> 'a1) -> 'a1

val monadFunctRel_jmdiscr :
  Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __

type monadFunctRel1 =
| Mk_MonadFunctRel1

val monadFunctRel1_rect_Type4 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel1 -> 'a1

val monadFunctRel1_rect_Type5 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel1 -> 'a1

val monadFunctRel1_rect_Type3 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel1 -> 'a1

val monadFunctRel1_rect_Type2 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel1 -> 'a1

val monadFunctRel1_rect_Type1 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel1 -> 'a1

val monadFunctRel1_rect_Type0 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadFunctRel1 -> 'a1

val monadFunctRel1_inv_rect_Type4 :
  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val monadFunctRel1_inv_rect_Type3 :
  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val monadFunctRel1_inv_rect_Type2 :
  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val monadFunctRel1_inv_rect_Type1 :
  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val monadFunctRel1_inv_rect_Type0 :
  Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val monadFunctRel1_jmdiscr :
  Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __

type monadGenRel =
| Mk_MonadGenRel

val monadGenRel_rect_Type4 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadGenRel -> 'a1

val monadGenRel_rect_Type5 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadGenRel -> 'a1

val monadGenRel_rect_Type3 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadGenRel -> 'a1

val monadGenRel_rect_Type2 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadGenRel -> 'a1

val monadGenRel_rect_Type1 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadGenRel -> 'a1

val monadGenRel_rect_Type0 :
  Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
  monadGenRel -> 'a1

val monadGenRel_inv_rect_Type4 :
  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val monadGenRel_inv_rect_Type3 :
  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val monadGenRel_inv_rect_Type2 :
  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val monadGenRel_inv_rect_Type1 :
  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val monadGenRel_inv_rect_Type0 :
  Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val monadGenRel_jmdiscr :
  Monad.monad -> Monad.monad -> monadGenRel -> monadGenRel -> __

val res_preserve : monadFunctRel

val res_preserve1 : monadFunctRel1

val gen_res_preserve : monadGenRel

val opt_preserve : monadFunctRel

val opt_preserve1 : monadFunctRel1

val gen_opt_preserve : monadGenRel

val io_preserve : monadFunctRel

val io_preserve1 : monadFunctRel1

val gen_io_preserve : monadGenRel