open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Relations

open Setoids

type ('a, 'b) pred_transformer = __

type ('a, 'b, 'c, 'd) rel_transformer = __

type monad = { m_return : (__ -> __ -> __);
               m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }

val monad_rect_Type4 :
  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  monad -> 'a1

val monad_rect_Type5 :
  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  monad -> 'a1

val monad_rect_Type3 :
  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  monad -> 'a1

val monad_rect_Type2 :
  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  monad -> 'a1

val monad_rect_Type1 :
  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  monad -> 'a1

val monad_rect_Type0 :
  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
  monad -> 'a1

type 'x_772 monad0 

val m_return0 : monad -> 'a1 -> __

val m_bind0 : monad -> __ -> ('a1 -> __) -> __

val monad_inv_rect_Type4 :
  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  __ -> 'a1) -> 'a1

val monad_inv_rect_Type3 :
  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  __ -> 'a1) -> 'a1

val monad_inv_rect_Type2 :
  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  __ -> 'a1) -> 'a1

val monad_inv_rect_Type1 :
  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  __ -> 'a1) -> 'a1

val monad_inv_rect_Type0 :
  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
  __ -> 'a1) -> 'a1

type monadProps =
  monad
  (* singleton inductive, whose constructor was mk_MonadProps *)

val monadProps_rect_Type4 :
  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1

val monadProps_rect_Type5 :
  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1

val monadProps_rect_Type3 :
  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1

val monadProps_rect_Type2 :
  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1

val monadProps_rect_Type1 :
  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1

val monadProps_rect_Type0 :
  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1

val max_def : monadProps -> monad

val monadProps_inv_rect_Type4 :
  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadProps_inv_rect_Type3 :
  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadProps_inv_rect_Type2 :
  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadProps_inv_rect_Type1 :
  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadProps_inv_rect_Type0 :
  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

type 'x_772 max_def__o__monad = __

type setoidMonadProps =
  monad
  (* singleton inductive, whose constructor was mk_SetoidMonadProps *)

val setoidMonadProps_rect_Type4 :
  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
  setoidMonadProps -> 'a1

val setoidMonadProps_rect_Type5 :
  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
  setoidMonadProps -> 'a1

val setoidMonadProps_rect_Type3 :
  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
  setoidMonadProps -> 'a1

val setoidMonadProps_rect_Type2 :
  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
  setoidMonadProps -> 'a1

val setoidMonadProps_rect_Type1 :
  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
  setoidMonadProps -> 'a1

val setoidMonadProps_rect_Type0 :
  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
  setoidMonadProps -> 'a1

val smax_def : setoidMonadProps -> monad

val setoidMonadProps_inv_rect_Type4 :
  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val setoidMonadProps_inv_rect_Type3 :
  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val setoidMonadProps_inv_rect_Type2 :
  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val setoidMonadProps_inv_rect_Type1 :
  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val setoidMonadProps_inv_rect_Type0 :
  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

type 'x_772 smax_def__o__monad = __

val setoid_of_monad : setoidMonadProps -> Setoids.setoid

open Bool

open Nat

open List

val m_map : monad -> ('a1 -> 'a2) -> __ -> __

val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __

val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __

val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __

val m_join : monad -> __ -> __

val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __

val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __

val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __

val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __

val m_fold : monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __

val makeMonadProps :
  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) -> monadProps

val makeSetoidMonadProps :
  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
  setoidMonadProps

open Jmeq

open Russell

type monadPred =
| Mk_MonadPred

val monadPred_rect_Type4 :
  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1

val monadPred_rect_Type5 :
  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1

val monadPred_rect_Type3 :
  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1

val monadPred_rect_Type2 :
  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1

val monadPred_rect_Type1 :
  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1

val monadPred_rect_Type0 :
  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1

val monadPred_inv_rect_Type4 :
  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadPred_inv_rect_Type3 :
  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadPred_inv_rect_Type2 :
  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadPred_inv_rect_Type1 :
  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadPred_inv_rect_Type0 :
  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __

type injMonadPred = { im_pred : monadPred;
                      mp_inject : (__ -> __ -> __ Types.sig0 -> __) }

val injMonadPred_rect_Type4 :
  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
  injMonadPred -> 'a1

val injMonadPred_rect_Type5 :
  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
  injMonadPred -> 'a1

val injMonadPred_rect_Type3 :
  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
  injMonadPred -> 'a1

val injMonadPred_rect_Type2 :
  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
  injMonadPred -> 'a1

val injMonadPred_rect_Type1 :
  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
  injMonadPred -> 'a1

val injMonadPred_rect_Type0 :
  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
  injMonadPred -> 'a1

val im_pred : monad -> injMonadPred -> monadPred

val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __

val injMonadPred_inv_rect_Type4 :
  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
  __ -> __ -> 'a1) -> 'a1

val injMonadPred_inv_rect_Type3 :
  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
  __ -> __ -> 'a1) -> 'a1

val injMonadPred_inv_rect_Type2 :
  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
  __ -> __ -> 'a1) -> 'a1

val injMonadPred_inv_rect_Type1 :
  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
  __ -> __ -> 'a1) -> 'a1

val injMonadPred_inv_rect_Type0 :
  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
  __ -> __ -> 'a1) -> 'a1

val injMonadPred_jmdiscr : monad -> injMonadPred -> injMonadPred -> __

type monadRel =
| Mk_MonadRel

val monadRel_rect_Type4 :
  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1

val monadRel_rect_Type5 :
  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1

val monadRel_rect_Type3 :
  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1

val monadRel_rect_Type2 :
  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1

val monadRel_rect_Type1 :
  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1

val monadRel_rect_Type0 :
  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1

val monadRel_inv_rect_Type4 :
  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadRel_inv_rect_Type3 :
  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadRel_inv_rect_Type2 :
  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadRel_inv_rect_Type1 :
  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadRel_inv_rect_Type0 :
  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __