open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open List

open Div_and_mod

open Jmeq

open Russell

open Util

(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type0_r a p x0 =
  Logic.eq_rect_r a x0 p

(** val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
let eq_rect_r2 a x x0 =
  (fun _ h -> h) __ x0

(** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type2_r a p x0 =
  eq_rect_r2 a x0 p

(** val dec_bounded_forall :
    (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
let dec_bounded_forall hP_dec k =
  Nat.nat_rect_Type0 (Types.Inl __) (fun k0 hind ->
    match hind with
    | Types.Inl _ ->
      (match hP_dec k0 with
       | Types.Inl _ -> Types.Inl __
       | Types.Inr _ -> Types.Inr __)
    | Types.Inr _ -> Types.Inr __) k

(** val dec_bounded_exists :
    (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
let dec_bounded_exists hP_dec k =
  Nat.nat_rect_Type0 (Types.Inr __) (fun k0 hind ->
    match hind with
    | Types.Inl _ -> Types.Inl __
    | Types.Inr _ ->
      (match hP_dec k0 with
       | Types.Inl _ -> Types.Inl __
       | Types.Inr _ -> Types.Inr __)) k

(** val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
let dec_true f h =
  match f with
  | Types.Inl x -> h x
  | Types.Inr _ -> assert false (* absurd case *)

(** val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
let dec_false f h =
  match f with
  | Types.Inl _ -> assert false (* absurd case *)
  | Types.Inr x -> h x