open Preamble

open Core_notation

open Pts

open Hints_declaration

val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2

val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2

val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_coerc : 'a1 -> 'a2

val true_rect_Type4 : 'a1 -> 'a1

val true_rect_Type5 : 'a1 -> 'a1

val true_rect_Type3 : 'a1 -> 'a1

val true_rect_Type2 : 'a1 -> 'a1

val true_rect_Type1 : 'a1 -> 'a1

val true_rect_Type0 : 'a1 -> 'a1

val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1

val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1

val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1

val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1

val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1

val true_discr : __ -> __

val false_rect_Type4 : __ -> 'a1

val false_rect_Type5 : __ -> 'a1

val false_rect_Type3 : __ -> 'a1

val false_rect_Type2 : __ -> 'a1

val false_rect_Type1 : __ -> 'a1

val false_rect_Type0 : __ -> 'a1

val not_rect_Type4 : (__ -> 'a1) -> 'a1

val not_rect_Type5 : (__ -> 'a1) -> 'a1

val not_rect_Type3 : (__ -> 'a1) -> 'a1

val not_rect_Type2 : (__ -> 'a1) -> 'a1

val not_rect_Type1 : (__ -> 'a1) -> 'a1

val not_rect_Type0 : (__ -> 'a1) -> 'a1

val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1

val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1

val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1

val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1

val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1

val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1

val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1

val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1

val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1

val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1

val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1

val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1

val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1

val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1

val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1

val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1

val r0 : 'a1 -> 'a1

val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2

val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3

val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4

val r4 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5

val streicherK : 'a1 -> 'a2 -> 'a2