29 val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
31 val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2
33 val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2
35 val dec_bounded_forall :
36 (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum
38 val dec_bounded_exists :
39 (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum
41 val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1
43 val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1