29 (** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
30 let eq_rect_Type0_r a p x0 =
31 Logic.eq_rect_r a x0 p
33 (** val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
34 let eq_rect_r2 a x x0 =
37 (** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
38 let eq_rect_Type2_r a p x0 =
41 (** val dec_bounded_forall :
42 (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
43 let dec_bounded_forall hP_dec k =
44 Nat.nat_rect_Type0 (Types.Inl __) (fun k0 hind ->
48 | Types.Inl _ -> Types.Inl __
49 | Types.Inr _ -> Types.Inr __)
50 | Types.Inr _ -> Types.Inr __) k
52 (** val dec_bounded_exists :
53 (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
54 let dec_bounded_exists hP_dec k =
55 Nat.nat_rect_Type0 (Types.Inr __) (fun k0 hind ->
57 | Types.Inl _ -> Types.Inl __
60 | Types.Inl _ -> Types.Inl __
61 | Types.Inr _ -> Types.Inr __)) k
63 (** val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
67 | Types.Inr _ -> assert false (* absurd case *)
69 (** val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
72 | Types.Inl _ -> assert false (* absurd case *)