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 **)
let rec monad_rect_Type4 h_mk_Monad x_744 =
  let { m_return = m_return0; m_bind = m_bind0 } = x_744 in
  h_mk_Monad __ m_return0 m_bind0

(** val monad_rect_Type5 :
    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    -> monad -> 'a1 **)
let rec monad_rect_Type5 h_mk_Monad x_746 =
  let { m_return = m_return0; m_bind = m_bind0 } = x_746 in
  h_mk_Monad __ m_return0 m_bind0

(** val monad_rect_Type3 :
    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    -> monad -> 'a1 **)
let rec monad_rect_Type3 h_mk_Monad x_748 =
  let { m_return = m_return0; m_bind = m_bind0 } = x_748 in
  h_mk_Monad __ m_return0 m_bind0

(** val monad_rect_Type2 :
    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    -> monad -> 'a1 **)
let rec monad_rect_Type2 h_mk_Monad x_750 =
  let { m_return = m_return0; m_bind = m_bind0 } = x_750 in
  h_mk_Monad __ m_return0 m_bind0

(** val monad_rect_Type1 :
    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    -> monad -> 'a1 **)
let rec monad_rect_Type1 h_mk_Monad x_752 =
  let { m_return = m_return0; m_bind = m_bind0 } = x_752 in
  h_mk_Monad __ m_return0 m_bind0

(** val monad_rect_Type0 :
    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    -> monad -> 'a1 **)
let rec monad_rect_Type0 h_mk_Monad x_754 =
  let { m_return = m_return0; m_bind = m_bind0 } = x_754 in
  h_mk_Monad __ m_return0 m_bind0

type 'x monad0 = __

(** val m_return0 : monad -> 'a1 -> __ **)
let rec m_return0 xxx x_771 =
  (let { m_return = yyy; m_bind = x0 } = xxx in Obj.magic yyy) __ x_771

(** val m_bind0 : monad -> __ -> ('a1 -> __) -> __ **)
let rec m_bind0 xxx x_768 x_769 =
  (let { m_return = x0; m_bind = yyy } = xxx in Obj.magic yyy) __ __ x_768
    x_769

(** val monad_inv_rect_Type4 :
    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
    -> __ -> 'a1) -> 'a1 **)
let monad_inv_rect_Type4 hterm h1 =
  let hcut = monad_rect_Type4 h1 hterm in hcut __

(** val monad_inv_rect_Type3 :
    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
    -> __ -> 'a1) -> 'a1 **)
let monad_inv_rect_Type3 hterm h1 =
  let hcut = monad_rect_Type3 h1 hterm in hcut __

(** val monad_inv_rect_Type2 :
    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
    -> __ -> 'a1) -> 'a1 **)
let monad_inv_rect_Type2 hterm h1 =
  let hcut = monad_rect_Type2 h1 hterm in hcut __

(** val monad_inv_rect_Type1 :
    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
    -> __ -> 'a1) -> 'a1 **)
let monad_inv_rect_Type1 hterm h1 =
  let hcut = monad_rect_Type1 h1 hterm in hcut __

(** val monad_inv_rect_Type0 :
    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
    -> __ -> 'a1) -> 'a1 **)
let monad_inv_rect_Type0 hterm h1 =
  let hcut = monad_rect_Type0 h1 hterm in hcut __

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

(** val monadProps_rect_Type4 :
    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
let rec monadProps_rect_Type4 h_mk_MonadProps x_775 =
  let max_def = x_775 in h_mk_MonadProps max_def __ __ __ __

(** val monadProps_rect_Type5 :
    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
let rec monadProps_rect_Type5 h_mk_MonadProps x_777 =
  let max_def = x_777 in h_mk_MonadProps max_def __ __ __ __

(** val monadProps_rect_Type3 :
    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
let rec monadProps_rect_Type3 h_mk_MonadProps x_779 =
  let max_def = x_779 in h_mk_MonadProps max_def __ __ __ __

(** val monadProps_rect_Type2 :
    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
let rec monadProps_rect_Type2 h_mk_MonadProps x_781 =
  let max_def = x_781 in h_mk_MonadProps max_def __ __ __ __

(** val monadProps_rect_Type1 :
    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
let rec monadProps_rect_Type1 h_mk_MonadProps x_783 =
  let max_def = x_783 in h_mk_MonadProps max_def __ __ __ __

(** val monadProps_rect_Type0 :
    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
let rec monadProps_rect_Type0 h_mk_MonadProps x_785 =
  let max_def = x_785 in h_mk_MonadProps max_def __ __ __ __

(** val max_def : monadProps -> monad **)
let rec max_def xxx =
  let yyy = xxx in yyy

(** val monadProps_inv_rect_Type4 :
    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadProps_inv_rect_Type4 hterm h1 =
  let hcut = monadProps_rect_Type4 h1 hterm in hcut __

(** val monadProps_inv_rect_Type3 :
    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadProps_inv_rect_Type3 hterm h1 =
  let hcut = monadProps_rect_Type3 h1 hterm in hcut __

(** val monadProps_inv_rect_Type2 :
    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadProps_inv_rect_Type2 hterm h1 =
  let hcut = monadProps_rect_Type2 h1 hterm in hcut __

(** val monadProps_inv_rect_Type1 :
    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadProps_inv_rect_Type1 hterm h1 =
  let hcut = monadProps_rect_Type1 h1 hterm in hcut __

(** val monadProps_inv_rect_Type0 :
    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadProps_inv_rect_Type0 hterm h1 =
  let hcut = monadProps_rect_Type0 h1 hterm in hcut __

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 **)
let rec setoidMonadProps_rect_Type4 h_mk_SetoidMonadProps x_807 =
  let smax_def = x_807 in
  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __

(** val setoidMonadProps_rect_Type5 :
    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    setoidMonadProps -> 'a1 **)
let rec setoidMonadProps_rect_Type5 h_mk_SetoidMonadProps x_809 =
  let smax_def = x_809 in
  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __

(** val setoidMonadProps_rect_Type3 :
    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    setoidMonadProps -> 'a1 **)
let rec setoidMonadProps_rect_Type3 h_mk_SetoidMonadProps x_811 =
  let smax_def = x_811 in
  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __

(** val setoidMonadProps_rect_Type2 :
    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    setoidMonadProps -> 'a1 **)
let rec setoidMonadProps_rect_Type2 h_mk_SetoidMonadProps x_813 =
  let smax_def = x_813 in
  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __

(** val setoidMonadProps_rect_Type1 :
    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    setoidMonadProps -> 'a1 **)
let rec setoidMonadProps_rect_Type1 h_mk_SetoidMonadProps x_815 =
  let smax_def = x_815 in
  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __

(** val setoidMonadProps_rect_Type0 :
    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    setoidMonadProps -> 'a1 **)
let rec setoidMonadProps_rect_Type0 h_mk_SetoidMonadProps x_817 =
  let smax_def = x_817 in
  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __

(** val smax_def : setoidMonadProps -> monad **)
let rec smax_def xxx =
  let yyy = xxx in yyy

(** val setoidMonadProps_inv_rect_Type4 :
    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoidMonadProps_inv_rect_Type4 hterm h1 =
  let hcut = setoidMonadProps_rect_Type4 h1 hterm in hcut __

(** val setoidMonadProps_inv_rect_Type3 :
    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoidMonadProps_inv_rect_Type3 hterm h1 =
  let hcut = setoidMonadProps_rect_Type3 h1 hterm in hcut __

(** val setoidMonadProps_inv_rect_Type2 :
    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoidMonadProps_inv_rect_Type2 hterm h1 =
  let hcut = setoidMonadProps_rect_Type2 h1 hterm in hcut __

(** val setoidMonadProps_inv_rect_Type1 :
    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoidMonadProps_inv_rect_Type1 hterm h1 =
  let hcut = setoidMonadProps_rect_Type1 h1 hterm in hcut __

(** val setoidMonadProps_inv_rect_Type0 :
    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoidMonadProps_inv_rect_Type0 hterm h1 =
  let hcut = setoidMonadProps_rect_Type0 h1 hterm in hcut __

type 'x_772 smax_def__o__monad = __

(** val setoid_of_monad : setoidMonadProps -> Setoids.setoid **)
let setoid_of_monad m =
  Setoids.Mk_Setoid

open Bool

open Nat

open List

(** val m_map : monad -> ('a1 -> 'a2) -> __ -> __ **)
let m_map m f m0 =
  m_bind0 m m0 (fun x -> m_return0 m (f x))

(** val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
let m_map2 m f m0 n =
  m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (f x y)))

(** val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __ **)
let m_bind2 m m0 f =
  m_bind0 m m0 (fun p -> f p.Types.fst p.Types.snd)

(** val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
let m_bind3 m m0 f =
  m_bind0 m m0 (fun p ->
    f p.Types.fst.Types.fst p.Types.fst.Types.snd p.Types.snd)

(** val m_join : monad -> __ -> __ **)
let m_join m m0 =
  m_bind0 m m0 (fun x -> x)

(** val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __ **)
let m_sigbind2 m e f =
  m_bind0 m e (fun e_sig ->
    let p = e_sig in
    (let { Types.fst = a; Types.snd = b } = p in (fun _ -> f a b __)) __)

(** val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
let m_list_map m f l =
  List.foldr (fun el macc ->
    m_bind0 m (f el) (fun r ->
      m_bind0 m macc (fun acc -> m_return0 m (List.Cons (r, acc)))))
    (m_return0 m List.Nil) l

(** val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
let m_list_map_sigma m f l =
  List.foldr (fun el macc ->
    m_bind0 m (f el) (fun eta285 ->
      let r = eta285 in
      m_bind0 m macc (fun eta284 ->
        let acc = eta284 in m_return0 m (List.Cons (r, acc)))))
    (m_return0 m List.Nil) l

(** val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
let m_bin_op m op m0 n =
  m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (op x y)))

(** val m_fold :
    monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __ **)
let rec m_fold m f l init =
  match l with
  | List.Nil -> m_return0 m init
  | List.Cons (hd, tl) -> m_bind0 m (f hd init) (fun y -> m_fold m f tl y)

(** val makeMonadProps :
    (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
    monadProps **)
let makeMonadProps m_return1 m_bind1 =
  { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }

(** val makeSetoidMonadProps :
    (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
    setoidMonadProps **)
let makeSetoidMonadProps m_return1 m_bind1 =
  { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }

open Jmeq

open Russell

type monadPred =
| Mk_MonadPred

(** val monadPred_rect_Type4 :
    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
let rec monadPred_rect_Type4 m h_mk_MonadPred = function
| Mk_MonadPred -> h_mk_MonadPred __ __ __ __

(** val monadPred_rect_Type5 :
    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
let rec monadPred_rect_Type5 m h_mk_MonadPred = function
| Mk_MonadPred -> h_mk_MonadPred __ __ __ __

(** val monadPred_rect_Type3 :
    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
let rec monadPred_rect_Type3 m h_mk_MonadPred = function
| Mk_MonadPred -> h_mk_MonadPred __ __ __ __

(** val monadPred_rect_Type2 :
    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
let rec monadPred_rect_Type2 m h_mk_MonadPred = function
| Mk_MonadPred -> h_mk_MonadPred __ __ __ __

(** val monadPred_rect_Type1 :
    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
let rec monadPred_rect_Type1 m h_mk_MonadPred = function
| Mk_MonadPred -> h_mk_MonadPred __ __ __ __

(** val monadPred_rect_Type0 :
    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
let rec monadPred_rect_Type0 m h_mk_MonadPred = function
| Mk_MonadPred -> h_mk_MonadPred __ __ __ __

(** val monadPred_inv_rect_Type4 :
    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadPred_inv_rect_Type4 x1 hterm h1 =
  let hcut = monadPred_rect_Type4 x1 h1 hterm in hcut __

(** val monadPred_inv_rect_Type3 :
    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadPred_inv_rect_Type3 x1 hterm h1 =
  let hcut = monadPred_rect_Type3 x1 h1 hterm in hcut __

(** val monadPred_inv_rect_Type2 :
    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadPred_inv_rect_Type2 x1 hterm h1 =
  let hcut = monadPred_rect_Type2 x1 h1 hterm in hcut __

(** val monadPred_inv_rect_Type1 :
    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadPred_inv_rect_Type1 x1 hterm h1 =
  let hcut = monadPred_rect_Type1 x1 h1 hterm in hcut __

(** val monadPred_inv_rect_Type0 :
    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadPred_inv_rect_Type0 x1 hterm h1 =
  let hcut = monadPred_rect_Type0 x1 h1 hterm in hcut __

(** val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __ **)
let monadPred_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let Mk_MonadPred = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y

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

(** val injMonadPred_rect_Type4 :
    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    injMonadPred -> 'a1 **)
let rec injMonadPred_rect_Type4 m h_mk_InjMonadPred x_1048 =
  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1048 in
  h_mk_InjMonadPred im_pred0 mp_inject0 __

(** val injMonadPred_rect_Type5 :
    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    injMonadPred -> 'a1 **)
let rec injMonadPred_rect_Type5 m h_mk_InjMonadPred x_1050 =
  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1050 in
  h_mk_InjMonadPred im_pred0 mp_inject0 __

(** val injMonadPred_rect_Type3 :
    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    injMonadPred -> 'a1 **)
let rec injMonadPred_rect_Type3 m h_mk_InjMonadPred x_1052 =
  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1052 in
  h_mk_InjMonadPred im_pred0 mp_inject0 __

(** val injMonadPred_rect_Type2 :
    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    injMonadPred -> 'a1 **)
let rec injMonadPred_rect_Type2 m h_mk_InjMonadPred x_1054 =
  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1054 in
  h_mk_InjMonadPred im_pred0 mp_inject0 __

(** val injMonadPred_rect_Type1 :
    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    injMonadPred -> 'a1 **)
let rec injMonadPred_rect_Type1 m h_mk_InjMonadPred x_1056 =
  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1056 in
  h_mk_InjMonadPred im_pred0 mp_inject0 __

(** val injMonadPred_rect_Type0 :
    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    injMonadPred -> 'a1 **)
let rec injMonadPred_rect_Type0 m h_mk_InjMonadPred x_1058 =
  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1058 in
  h_mk_InjMonadPred im_pred0 mp_inject0 __

(** val im_pred : monad -> injMonadPred -> monadPred **)
let rec im_pred m xxx =
  xxx.im_pred

(** val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __ **)
let rec mp_inject0 m xxx x_1073 =
  (xxx.mp_inject) __ __ x_1073

(** val injMonadPred_inv_rect_Type4 :
    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
    -> __ -> __ -> 'a1) -> 'a1 **)
let injMonadPred_inv_rect_Type4 x1 hterm h1 =
  let hcut = injMonadPred_rect_Type4 x1 h1 hterm in hcut __

(** val injMonadPred_inv_rect_Type3 :
    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
    -> __ -> __ -> 'a1) -> 'a1 **)
let injMonadPred_inv_rect_Type3 x1 hterm h1 =
  let hcut = injMonadPred_rect_Type3 x1 h1 hterm in hcut __

(** val injMonadPred_inv_rect_Type2 :
    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
    -> __ -> __ -> 'a1) -> 'a1 **)
let injMonadPred_inv_rect_Type2 x1 hterm h1 =
  let hcut = injMonadPred_rect_Type2 x1 h1 hterm in hcut __

(** val injMonadPred_inv_rect_Type1 :
    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
    -> __ -> __ -> 'a1) -> 'a1 **)
let injMonadPred_inv_rect_Type1 x1 hterm h1 =
  let hcut = injMonadPred_rect_Type1 x1 h1 hterm in hcut __

(** val injMonadPred_inv_rect_Type0 :
    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
    -> __ -> __ -> 'a1) -> 'a1 **)
let injMonadPred_inv_rect_Type0 x1 hterm h1 =
  let hcut = injMonadPred_rect_Type0 x1 h1 hterm in hcut __

(** val injMonadPred_jmdiscr :
    monad -> injMonadPred -> injMonadPred -> __ **)
let injMonadPred_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let { im_pred = a0; mp_inject = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

type monadRel =
| Mk_MonadRel

(** val monadRel_rect_Type4 :
    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
let rec monadRel_rect_Type4 m1 m2 h_mk_MonadRel = function
| Mk_MonadRel -> h_mk_MonadRel __ __ __ __

(** val monadRel_rect_Type5 :
    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
let rec monadRel_rect_Type5 m1 m2 h_mk_MonadRel = function
| Mk_MonadRel -> h_mk_MonadRel __ __ __ __

(** val monadRel_rect_Type3 :
    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
let rec monadRel_rect_Type3 m1 m2 h_mk_MonadRel = function
| Mk_MonadRel -> h_mk_MonadRel __ __ __ __

(** val monadRel_rect_Type2 :
    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
let rec monadRel_rect_Type2 m1 m2 h_mk_MonadRel = function
| Mk_MonadRel -> h_mk_MonadRel __ __ __ __

(** val monadRel_rect_Type1 :
    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
let rec monadRel_rect_Type1 m1 m2 h_mk_MonadRel = function
| Mk_MonadRel -> h_mk_MonadRel __ __ __ __

(** val monadRel_rect_Type0 :
    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
let rec monadRel_rect_Type0 m1 m2 h_mk_MonadRel = function
| Mk_MonadRel -> h_mk_MonadRel __ __ __ __

(** val monadRel_inv_rect_Type4 :
    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadRel_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = monadRel_rect_Type4 x1 x2 h1 hterm in hcut __

(** val monadRel_inv_rect_Type3 :
    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadRel_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = monadRel_rect_Type3 x1 x2 h1 hterm in hcut __

(** val monadRel_inv_rect_Type2 :
    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadRel_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = monadRel_rect_Type2 x1 x2 h1 hterm in hcut __

(** val monadRel_inv_rect_Type1 :
    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadRel_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = monadRel_rect_Type1 x1 x2 h1 hterm in hcut __

(** val monadRel_inv_rect_Type0 :
    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let monadRel_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = monadRel_rect_Type0 x1 x2 h1 hterm in hcut __

(** val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __ **)
let monadRel_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (let Mk_MonadRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y