tt('type/enumeral/bl', ty, $t > $t).
tt('type/enumeral/bt', ty, $t > $t).
tt('const/enumeral/BL_ACCUM', ty, ![A : $t]: (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > ('type/enumeral/bl' A))))).
tt('const/enumeral/BL_CONS', ty, ![A : $t]: (A > (('type/enumeral/bl' A) > ('type/enumeral/bl' A)))).
tt('const/enumeral/ENUMERAL', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > (A > $o)))).
tt('const/enumeral/K2', ty, ![A : $t]: (A > 'type/num/num')).
tt('const/enumeral/LESS_ALL', ty, ![A : $t]: (('type/toto/toto' A) > (A > ((A > $o) > $o)))).
tt('const/enumeral/OL', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > $o))).
tt('const/enumeral/OL_bt', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > $o))).
tt('const/enumeral/OL_bt_lb', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > $o)))).
tt('const/enumeral/OL_bt_lb_ub', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > (A > $o))))).
tt('const/enumeral/OL_bt_ub', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > (A > $o)))).
tt('const/enumeral/OL_sublists', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o))).
tt('const/enumeral/OL_sublists_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) > $o)).
tt('const/enumeral/OU', ty, ![A : $t]: (('type/toto/toto' A) > ((A > $o) > ((A > $o) > (A > $o))))).
tt('const/enumeral/OWL', ty, ![A : $t]: (('type/toto/toto' A) > ((A > $o) > (('type/list/list' A) > $o)))).
tt('const/enumeral/UO', ty, ![A : $t]: (('type/toto/toto' A) > ((A > $o) > ((A > $o) > (A > $o))))).
tt('const/enumeral/bl_CASE', ty, ![A : $t, B : $t]: (('type/enumeral/bl' A) > (B > ((('type/enumeral/bl' A) > B) > ((A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > B))) > B))))).
tt('const/enumeral/bl_rev', ty, ![A : $t]: (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > ('type/enumeral/bt' A)))).
tt('const/enumeral/bl_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/enumeral/bl' A) > 'type/num/num'))).
tt('const/enumeral/bl_to_bt', ty, ![A : $t]: (('type/enumeral/bl' A) > ('type/enumeral/bt' A))).
tt('const/enumeral/bl_to_set', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bl' A) > (A > $o)))).
tt('const/enumeral/bt_CASE', ty, ![A : $t, B : $t]: (('type/enumeral/bt' A) > (B > ((('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > B))) > B)))).
tt('const/enumeral/bt_rev', ty, ![A : $t]: (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > ('type/enumeral/bl' A)))).
tt('const/enumeral/bt_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/enumeral/bt' A) > 'type/num/num'))).
tt('const/enumeral/bt_to_bl', ty, ![A : $t]: (('type/enumeral/bt' A) > ('type/enumeral/bl' A))).
tt('const/enumeral/bt_to_list', ty, ![A : $t]: (('type/enumeral/bt' A) > ('type/list/list' A))).
tt('const/enumeral/bt_to_list_ac', ty, ![A : $t]: (('type/enumeral/bt' A) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/enumeral/bt_to_ol', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > ('type/list/list' A)))).
tt('const/enumeral/bt_to_ol_ac', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/enumeral/bt_to_ol_lb', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > ('type/list/list' A))))).
tt('const/enumeral/bt_to_ol_lb_ac', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > (('type/list/list' A) > ('type/list/list' A)))))).
tt('const/enumeral/bt_to_ol_lb_ub', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > (A > ('type/list/list' A)))))).
tt('const/enumeral/bt_to_ol_lb_ub_ac', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > (A > (('type/list/list' A) > ('type/list/list' A))))))).
tt('const/enumeral/bt_to_ol_ub', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > (A > ('type/list/list' A))))).
tt('const/enumeral/bt_to_ol_ub_ac', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > (A > (('type/list/list' A) > ('type/list/list' A)))))).
tt('const/enumeral/bt_to_set_lb', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > (A > $o))))).
tt('const/enumeral/bt_to_set_lb_ub', ty, ![A : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' A) > (A > (A > $o)))))).
tt('const/enumeral/bt_to_set_ub', ty, ![A : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' A) > (A > (A > $o))))).
tt('const/enumeral/incr_sbuild', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > ('type/list/list' ('type/option/option' ('type/list/list' A)))))).
tt('const/enumeral/incr_smerge', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > ('type/list/list' ('type/option/option' ('type/list/list' A))))))).
tt('const/enumeral/incr_smerge_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > ('type/list/list' ('type/option/option' ('type/list/list' A))))).
tt('const/enumeral/incr_ssort', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/enumeral/list_to_bl', ty, ![A : $t]: (('type/list/list' A) > ('type/enumeral/bl' A))).
tt('const/enumeral/list_to_bt', ty, ![C : $t]: (('type/list/list' C) > ('type/enumeral/bt' C))).
tt('const/enumeral/lol_set', ty, ![A : $t]: (('type/list/list' ('type/option/option' ('type/list/list' A))) > (A > $o))).
tt('const/enumeral/nbl', ty, ![A : $t]: ('type/enumeral/bl' A)).
tt('const/enumeral/node', ty, ![A : $t]: (('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > ('type/enumeral/bt' A))))).
tt('const/enumeral/nt', ty, ![A : $t]: ('type/enumeral/bt' A)).
tt('const/enumeral/onebl', ty, ![A : $t]: (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > ('type/enumeral/bl' A))))).
tt('const/enumeral/sdiff', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/enumeral/sdiff_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > ('type/list/list' A))).
tt('const/enumeral/sinter', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/enumeral/sinter_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > ('type/list/list' A))).
tt('const/enumeral/smerge', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/enumeral/smerge_out', ty, ![A : $t]: (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > ('type/list/list' A))))).
tt('const/enumeral/smerge_out_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > ('type/list/list' A))).
tt('const/enumeral/smerge_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > ('type/list/list' A))).
tt('const/enumeral/zerbl', ty, ![A : $t]: (('type/enumeral/bl' A) > ('type/enumeral/bl' A))).
tt('thm/enumeral/bt_TY_DEF_', def, ![A : $t]: (?[rep : (('type/enumeral/bt' A) > ('type/ind_type/recspace' A))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' A) ('type/enumeral/bt' A)) (^['a0\'' : ('type/ind_type/recspace' A)]: (!['\'bt\'' : (('type/ind_type/recspace' A) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' A)]: ((('a0\'0' = (('const/ind_type/CONSTR' A) 'const/num/0' ('const/bool/ARB' A) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))) | (?[a0 : ('type/ind_type/recspace' A), a1 : A, a2 : ('type/ind_type/recspace' A)]: (('a0\'0' = ((^[a00 : ('type/ind_type/recspace' A), a10 : A, a20 : ('type/ind_type/recspace' A)]: (('const/ind_type/CONSTR' A) ('const/num/SUC' 'const/num/0') a10 (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a00 (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a20 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))))) a0 a1 a2)) & (('\'bt\'' a0) & ('\'bt\'' a2))))) => ('\'bt\'' 'a0\'0'))) => ('\'bt\'' 'a0\'')))) rep))).
tt('thm/enumeral/bt_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/enumeral/bt_size' A) f ('const/enumeral/nt' A)) = 'const/num/0'))).
tt('thm/enumeral/bt_size_def_e1', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : ('type/enumeral/bt' A), a1 : A, a2 : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_size' A) f (('const/enumeral/node' A) a0 a1 a2)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (('const/enumeral/bt_size' A) f a0) ('const/arithmetic/+' (f a1) (('const/enumeral/bt_size' A) f a2))))))).
tt('thm/enumeral/datatype_bt_', ax, ![A : $t]: (![bt : (('type/enumeral/bt' A) > ((('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > ('type/enumeral/bt' A)))) > $o))]: (('const/bool/DATATYPE' $o) (bt ('const/enumeral/nt' A) ('const/enumeral/node' A))))).
tt('thm/enumeral/bt_case_cong_', ax, ![A : $t, B : $t]: (!['v\'' : B, 'f\'' : (('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > B))), M : ('type/enumeral/bt' A), 'M\'' : ('type/enumeral/bt' A), v : B, f : (('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > B)))]: (((M = 'M\'') & ((('M\'' = ('const/enumeral/nt' A)) => (v = 'v\'')) & (![a0 : ('type/enumeral/bt' A), a1 : A, a2 : ('type/enumeral/bt' A)]: (('M\'' = (('const/enumeral/node' A) a0 a1 a2)) => ((f a0 a1 a2) = ('f\'' a0 a1 a2)))))) => ((('const/enumeral/bt_CASE' A B) M v f) = (('const/enumeral/bt_CASE' A B) 'M\'' 'v\'' 'f\''))))).
tt('thm/enumeral/bt_nchotomy_', ax, ![A : $t]: (![bb : ('type/enumeral/bt' A)]: ((bb = ('const/enumeral/nt' A)) | (?[b : ('type/enumeral/bt' A), a : A, b0 : ('type/enumeral/bt' A)]: (bb = (('const/enumeral/node' A) b a b0)))))).
tt('thm/enumeral/bt_Axiom_', ax, ![A : $t, B : $t]: (![f0 : B, f1 : (A > (('type/enumeral/bt' A) > (('type/enumeral/bt' A) > (B > (B > B)))))]: (?[fn : (('type/enumeral/bt' A) > B)]: (((fn ('const/enumeral/nt' A)) = f0) & (![a0 : ('type/enumeral/bt' A), a1 : A, a2 : ('type/enumeral/bt' A)]: ((fn (('const/enumeral/node' A) a0 a1 a2)) = (f1 a1 a0 a2 (fn a0) (fn a2)))))))).
tt('thm/enumeral/bt_induction_', ax, ![A : $t]: (![P : (('type/enumeral/bt' A) > $o)]: (((P ('const/enumeral/nt' A)) & (![b : ('type/enumeral/bt' A), b0 : ('type/enumeral/bt' A)]: (((P b) & (P b0)) => (![a : A]: (P (('const/enumeral/node' A) b a b0)))))) => (![b : ('type/enumeral/bt' A)]: (P b))))).
tt('thm/enumeral/bl_TY_DEF_', def, ![A : $t]: (?[rep : (('type/enumeral/bl' A) > ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A))))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A))) ('type/enumeral/bl' A)) (^['a0\'' : ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))]: (!['\'bl\'' : (('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A))) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))]: ((('a0\'0' = (('const/ind_type/CONSTR' ('type/pair/prod' A ('type/enumeral/bt' A))) 'const/num/0' (('const/pair/,' A ('type/enumeral/bt' A)) ('const/bool/ARB' A) ('const/bool/ARB' ('type/enumeral/bt' A))) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' A ('type/enumeral/bt' A)))))) | ((?[a : ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))]: (('a0\'0' = ((^[a0 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))]: (('const/ind_type/CONSTR' ('type/pair/prod' A ('type/enumeral/bt' A))) ('const/num/SUC' 'const/num/0') (('const/pair/,' A ('type/enumeral/bt' A)) ('const/bool/ARB' A) ('const/bool/ARB' ('type/enumeral/bt' A))) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))) a0 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' A ('type/enumeral/bt' A))))))) a)) & ('\'bl\'' a))) | (?[a0 : A, a1 : ('type/enumeral/bt' A), a2 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))]: (('a0\'0' = ((^[a00 : A, a10 : ('type/enumeral/bt' A), a20 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))]: (('const/ind_type/CONSTR' ('type/pair/prod' A ('type/enumeral/bt' A))) ('const/num/SUC' ('const/num/SUC' 'const/num/0')) (('const/pair/,' A ('type/enumeral/bt' A)) a00 a10) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' A ('type/enumeral/bt' A)))) a20 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' A ('type/enumeral/bt' A))))))) a0 a1 a2)) & ('\'bl\'' a2))))) => ('\'bl\'' 'a0\'0'))) => ('\'bl\'' 'a0\'')))) rep))).
tt('thm/enumeral/bl_case_def_0', def, ![B : $t, A : $t]: (![v : B, f : (('type/enumeral/bl' A) > B), f1 : (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > B)))]: ((('const/enumeral/bl_CASE' A B) ('const/enumeral/nbl' A) v f f1) = v))).
tt('thm/enumeral/bl_case_def_1', def, ![A : $t, B : $t]: (![a : ('type/enumeral/bl' A), v : B, f : (('type/enumeral/bl' A) > B), f1 : (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > B)))]: ((('const/enumeral/bl_CASE' A B) (('const/enumeral/zerbl' A) a) v f f1) = (f a)))).
tt('thm/enumeral/bl_case_def_e2', def, ![A : $t, B : $t]: (![a0 : A, a1 : ('type/enumeral/bt' A), a2 : ('type/enumeral/bl' A), v : B, f : (('type/enumeral/bl' A) > B), f1 : (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > B)))]: ((('const/enumeral/bl_CASE' A B) (('const/enumeral/onebl' A) a0 a1 a2) v f f1) = (f1 a0 a1 a2)))).
tt('thm/enumeral/bl_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/enumeral/bl_size' A) f ('const/enumeral/nbl' A)) = 'const/num/0'))).
tt('thm/enumeral/bl_size_def_1', def, ![A : $t]: (![f : (A > 'type/num/num'), a : ('type/enumeral/bl' A)]: ((('const/enumeral/bl_size' A) f (('const/enumeral/zerbl' A) a)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/enumeral/bl_size' A) f a))))).
tt('thm/enumeral/bl_size_def_e2', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : A, a1 : ('type/enumeral/bt' A), a2 : ('type/enumeral/bl' A)]: ((('const/enumeral/bl_size' A) f (('const/enumeral/onebl' A) a0 a1 a2)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (f a0) ('const/arithmetic/+' (('const/enumeral/bt_size' A) f a1) (('const/enumeral/bl_size' A) f a2))))))).
tt('thm/enumeral/datatype_bl_', ax, ![A : $t]: (![bl : (('type/enumeral/bl' A) > ((('type/enumeral/bl' A) > ('type/enumeral/bl' A)) > ((A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > ('type/enumeral/bl' A)))) > $o)))]: (('const/bool/DATATYPE' $o) (bl ('const/enumeral/nbl' A) ('const/enumeral/zerbl' A) ('const/enumeral/onebl' A))))).
tt('thm/enumeral/bl_11_0', ax, ![A : $t]: (![a : ('type/enumeral/bl' A), 'a\'' : ('type/enumeral/bl' A)]: (((('const/enumeral/zerbl' A) a) = (('const/enumeral/zerbl' A) 'a\'')) = (a = 'a\'')))).
tt('thm/enumeral/bl_11_e1', ax, ![A : $t]: (![a0 : A, a1 : ('type/enumeral/bt' A), a2 : ('type/enumeral/bl' A), 'a0\'' : A, 'a1\'' : ('type/enumeral/bt' A), 'a2\'' : ('type/enumeral/bl' A)]: (((('const/enumeral/onebl' A) a0 a1 a2) = (('const/enumeral/onebl' A) 'a0\'' 'a1\'' 'a2\'')) = ((a0 = 'a0\'') & ((a1 = 'a1\'') & (a2 = 'a2\'')))))).
tt('thm/enumeral/bl_distinct_0', ax, ![A : $t]: (![a : ('type/enumeral/bl' A)]: (~ (('const/enumeral/nbl' A) = (('const/enumeral/zerbl' A) a))))).
tt('thm/enumeral/bl_distinct_1', ax, ![A : $t]: (![a2 : ('type/enumeral/bl' A), a1 : ('type/enumeral/bt' A), a0 : A]: (~ (('const/enumeral/nbl' A) = (('const/enumeral/onebl' A) a0 a1 a2))))).
tt('thm/enumeral/bl_distinct_e2', ax, ![A : $t]: (![a2 : ('type/enumeral/bl' A), a1 : ('type/enumeral/bt' A), a0 : A, a : ('type/enumeral/bl' A)]: (~ ((('const/enumeral/zerbl' A) a) = (('const/enumeral/onebl' A) a0 a1 a2))))).
tt('thm/enumeral/bl_case_cong_', ax, ![A : $t, B : $t]: (!['v\'' : B, 'f1\'' : (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > B))), 'f\'' : (('type/enumeral/bl' A) > B), M : ('type/enumeral/bl' A), 'M\'' : ('type/enumeral/bl' A), v : B, f : (('type/enumeral/bl' A) > B), f1 : (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > B)))]: (((M = 'M\'') & ((('M\'' = ('const/enumeral/nbl' A)) => (v = 'v\'')) & ((![a : ('type/enumeral/bl' A)]: (('M\'' = (('const/enumeral/zerbl' A) a)) => ((f a) = ('f\'' a)))) & (![a0 : A, a1 : ('type/enumeral/bt' A), a2 : ('type/enumeral/bl' A)]: (('M\'' = (('const/enumeral/onebl' A) a0 a1 a2)) => ((f1 a0 a1 a2) = ('f1\'' a0 a1 a2))))))) => ((('const/enumeral/bl_CASE' A B) M v f f1) = (('const/enumeral/bl_CASE' A B) 'M\'' 'v\'' 'f\'' 'f1\''))))).
tt('thm/enumeral/bl_nchotomy_', ax, ![A : $t]: (![bb : ('type/enumeral/bl' A)]: ((bb = ('const/enumeral/nbl' A)) | ((?[b : ('type/enumeral/bl' A)]: (bb = (('const/enumeral/zerbl' A) b))) | (?[a : A, b0 : ('type/enumeral/bt' A), b : ('type/enumeral/bl' A)]: (bb = (('const/enumeral/onebl' A) a b0 b))))))).
tt('thm/enumeral/bl_Axiom_', ax, ![A : $t, B : $t]: (![f0 : B, f1 : (('type/enumeral/bl' A) > (B > B)), f2 : (A > (('type/enumeral/bt' A) > (('type/enumeral/bl' A) > (B > B))))]: (?[fn : (('type/enumeral/bl' A) > B)]: (((fn ('const/enumeral/nbl' A)) = f0) & ((![a : ('type/enumeral/bl' A)]: ((fn (('const/enumeral/zerbl' A) a)) = (f1 a (fn a)))) & (![a0 : A, a1 : ('type/enumeral/bt' A), a2 : ('type/enumeral/bl' A)]: ((fn (('const/enumeral/onebl' A) a0 a1 a2)) = (f2 a0 a1 a2 (fn a2))))))))).
tt('thm/enumeral/bl_induction_', ax, ![A : $t]: (![P : (('type/enumeral/bl' A) > $o)]: (((P ('const/enumeral/nbl' A)) & ((![b : ('type/enumeral/bl' A)]: ((P b) => (P (('const/enumeral/zerbl' A) b)))) & (![b : ('type/enumeral/bl' A)]: ((P b) => (![b0 : ('type/enumeral/bt' A), a : A]: (P (('const/enumeral/onebl' A) a b0 b))))))) => (![b : ('type/enumeral/bl' A)]: (P b))))).
tt('thm/enumeral/bt_11_', ax, ![A : $t]: (![a0 : ('type/enumeral/bt' A), a1 : A, a2 : ('type/enumeral/bt' A), 'a0\'' : ('type/enumeral/bt' A), 'a1\'' : A, 'a2\'' : ('type/enumeral/bt' A)]: (((('const/enumeral/node' A) a0 a1 a2) = (('const/enumeral/node' A) 'a0\'' 'a1\'' 'a2\'')) = ((a0 = 'a0\'') & ((a1 = 'a1\'') & (a2 = 'a2\'')))))).
tt('thm/enumeral/bt_distinct_', ax, ![A : $t]: (![a2 : ('type/enumeral/bt' A), a1 : A, a0 : ('type/enumeral/bt' A)]: (~ (('const/enumeral/nt' A) = (('const/enumeral/node' A) a0 a1 a2))))).
tt('thm/enumeral/bt_case_def_0', ax, ![B : $t, A : $t]: (![v : B, f : (('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > B)))]: ((('const/enumeral/bt_CASE' A B) ('const/enumeral/nt' A) v f) = v))).
tt('thm/enumeral/bt_case_def_e1', ax, ![A : $t, B : $t]: (![a0 : ('type/enumeral/bt' A), a1 : A, a2 : ('type/enumeral/bt' A), v : B, f : (('type/enumeral/bt' A) > (A > (('type/enumeral/bt' A) > B)))]: ((('const/enumeral/bt_CASE' A B) (('const/enumeral/node' A) a0 a1 a2) v f) = (f a0 a1 a2)))).
tt('thm/enumeral/BL_ACCUM_0', def, ![A : $t]: (![a : A, ac : ('type/enumeral/bt' A)]: ((('const/enumeral/BL_ACCUM' A) a ac ('const/enumeral/nbl' A)) = (('const/enumeral/onebl' A) a ac ('const/enumeral/nbl' A))))).
tt('thm/enumeral/BL_ACCUM_1', def, ![A : $t]: (![a : A, ac : ('type/enumeral/bt' A), bl : ('type/enumeral/bl' A)]: ((('const/enumeral/BL_ACCUM' A) a ac (('const/enumeral/zerbl' A) bl)) = (('const/enumeral/onebl' A) a ac bl)))).
tt('thm/enumeral/BL_ACCUM_e2', def, ![A : $t]: (![a : A, ac : ('type/enumeral/bt' A), r : A, rft : ('type/enumeral/bt' A), bl : ('type/enumeral/bl' A)]: ((('const/enumeral/BL_ACCUM' A) a ac (('const/enumeral/onebl' A) r rft bl)) = (('const/enumeral/zerbl' A) (('const/enumeral/BL_ACCUM' A) a (('const/enumeral/node' A) ac r rft) bl))))).
tt('thm/enumeral/BL_CONS_', def, ![A : $t]: (![a : A, bl : ('type/enumeral/bl' A)]: ((('const/enumeral/BL_CONS' A) a bl) = (('const/enumeral/BL_ACCUM' A) a ('const/enumeral/nt' A) bl)))).
tt('thm/enumeral/list_to_bl_0', def, ![A : $t]: ((('const/enumeral/list_to_bl' A) ('const/list/NIL' A)) = ('const/enumeral/nbl' A))).
tt('thm/enumeral/list_to_bl_e1', def, ![A : $t]: (![a : A, l : ('type/list/list' A)]: ((('const/enumeral/list_to_bl' A) (('const/list/CONS' A) a l)) = (('const/enumeral/BL_CONS' A) a (('const/enumeral/list_to_bl' A) l))))).
tt('thm/enumeral/bt_to_list_0', def, ![A : $t]: ((('const/enumeral/bt_to_list' A) ('const/enumeral/nt' A)) = ('const/list/NIL' A))).
tt('thm/enumeral/bt_to_list_e1', def, ![A : $t]: (![l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_list' A) (('const/enumeral/node' A) l x r)) = (('const/list/APPEND' A) (('const/list/APPEND' A) (('const/enumeral/bt_to_list' A) l) (('const/list/CONS' A) x ('const/list/NIL' A))) (('const/enumeral/bt_to_list' A) r))))).
tt('thm/enumeral/bt_to_list_ac_0', def, ![A : $t]: (![m : ('type/list/list' A)]: ((('const/enumeral/bt_to_list_ac' A) ('const/enumeral/nt' A) m) = m))).
tt('thm/enumeral/bt_to_list_ac_e1', def, ![A : $t]: (![l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), m : ('type/list/list' A)]: ((('const/enumeral/bt_to_list_ac' A) (('const/enumeral/node' A) l x r) m) = (('const/enumeral/bt_to_list_ac' A) l (('const/list/CONS' A) x (('const/enumeral/bt_to_list_ac' A) r m)))))).
tt('thm/enumeral/bt_to_list_thm_', ax, ![A : $t]: (![t : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_list' A) t) = (('const/enumeral/bt_to_list_ac' A) t ('const/list/NIL' A))))).
tt('thm/enumeral/bt_rev_0', def, ![A : $t]: (![bl : ('type/enumeral/bl' A)]: ((('const/enumeral/bt_rev' A) ('const/enumeral/nt' A) bl) = bl))).
tt('thm/enumeral/bt_rev_e1', def, ![A : $t]: (![lft : ('type/enumeral/bt' A), r : A, rft : ('type/enumeral/bt' A), bl : ('type/enumeral/bl' A)]: ((('const/enumeral/bt_rev' A) (('const/enumeral/node' A) lft r rft) bl) = (('const/enumeral/bt_rev' A) lft (('const/enumeral/onebl' A) r rft bl))))).
tt('thm/enumeral/K2_', def, ![A : $t]: (![a : A]: ((('const/enumeral/K2' A) a) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))).
tt('thm/enumeral/bl_rev_0', def, ![A : $t]: (![ft : ('type/enumeral/bt' A)]: ((('const/enumeral/bl_rev' A) ft ('const/enumeral/nbl' A)) = ft))).
tt('thm/enumeral/bl_rev_1', def, ![A : $t]: (![ft : ('type/enumeral/bt' A), b : ('type/enumeral/bl' A)]: ((('const/enumeral/bl_rev' A) ft (('const/enumeral/zerbl' A) b)) = (('const/enumeral/bl_rev' A) ft b)))).
tt('thm/enumeral/bl_rev_e2', def, ![A : $t]: (![ft : ('type/enumeral/bt' A), a : A, f : ('type/enumeral/bt' A), b : ('type/enumeral/bl' A)]: ((('const/enumeral/bl_rev' A) ft (('const/enumeral/onebl' A) a f b)) = (('const/enumeral/bl_rev' A) (('const/enumeral/node' A) ft a f) b)))).
tt('thm/enumeral/bl_to_bt_', def, ![A : $t]: (('const/enumeral/bl_to_bt' A) = (('const/enumeral/bl_rev' A) ('const/enumeral/nt' A)))).
tt('thm/enumeral/bt_to_bl_', def, ![A : $t]: (![t : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_bl' A) t) = (('const/enumeral/bt_rev' A) t ('const/enumeral/nbl' A))))).
tt('thm/enumeral/list_to_bt_', def, ![C : $t]: (![l : ('type/list/list' C)]: ((('const/enumeral/list_to_bt' C) l) = (('const/enumeral/bl_to_bt' C) (('const/enumeral/list_to_bl' C) l))))).
tt('thm/enumeral/OL_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/OL' A) cmp ('const/list/NIL' A)) = $true))).
tt('thm/enumeral/OL_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), a : A, l : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp (('const/list/CONS' A) a l)) = ((('const/enumeral/OL' A) cmp l) & (![p : A]: ((('const/bool/IN' A) p (('const/list/LIST_TO_SET' A) l)) => ((('const/toto/apto' A) cmp a p) = 'const/toto/LESS'))))))).
tt('thm/enumeral/smerge_tupled_primitive_', def, ![A : $t]: (('const/enumeral/smerge_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) ('type/list/list' A)) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))) R) & ((![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/EQUAL') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)))))) & ((![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)))))) & (![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l (('const/list/CONS' A) y m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m))))))))))) (^[smerge_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > ('type/list/list' A)), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/list/list' A) ('type/list/list' A)) v1 (^[v2 : ('type/list/list' A), v3 : ('type/list/list' A)]: (('const/list/list_CASE' A ('type/list/list' A)) v2 (('const/list/list_CASE' A ('type/list/list' A)) v3 (('const/combin/I' ('type/list/list' A)) ('const/list/NIL' A)) (^[y : A, m : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' A)) (('const/list/CONS' A) y m)))) (^[x : A, l : ('type/list/list' A)]: (('const/list/list_CASE' A ('type/list/list' A)) v3 (('const/combin/I' ('type/list/list' A)) (('const/list/CONS' A) x l)) (^['y\'' : A, 'm\'' : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' A)) (('const/toto/cpn_CASE' ('type/list/list' A)) (('const/toto/apto' A) cmp x 'y\'') (('const/list/CONS' A) x (smerge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l (('const/list/CONS' A) 'y\'' 'm\''))))) (('const/list/CONS' A) x (smerge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l 'm\'')))) (('const/list/CONS' A) 'y\'' (smerge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) 'm\'')))))))))))))))))).
tt('thm/enumeral/smerge_curried_', def, ![A : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' A), x2 : ('type/list/list' A)]: ((('const/enumeral/smerge' A) x x1 x2) = (('const/enumeral/smerge_tupled' A) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) x (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) x1 x2)))))).
tt('thm/enumeral/smerge_ind_', ax, ![A : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' A) > $o)))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' A) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A)]: (P cmp (('const/list/CONS' A) x l) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), y : A, m : ('type/list/list' A)]: (P cmp ('const/list/NIL' A) (('const/list/CONS' A) y m))) & (![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A), y : A, m : ('type/list/list' A)]: (((((('const/toto/apto' A) cmp x y) = 'const/toto/EQUAL') => (P cmp l m)) & ((((('const/toto/apto' A) cmp x y) = 'const/toto/GREATER') => (P cmp (('const/list/CONS' A) x l) m)) & (((('const/toto/apto' A) cmp x y) = 'const/toto/LESS') => (P cmp l (('const/list/CONS' A) y m))))) => (P cmp (('const/list/CONS' A) x l) (('const/list/CONS' A) y m))))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' A), v2 : ('type/list/list' A)]: (P v v1 v2))))).
tt('thm/enumeral/smerge_0', ax, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge' A) cmp ('const/list/NIL' A) ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/enumeral/smerge_1', ax, ![A : $t]: (![x : A, l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge' A) cmp (('const/list/CONS' A) x l) ('const/list/NIL' A)) = (('const/list/CONS' A) x l)))).
tt('thm/enumeral/smerge_2', ax, ![A : $t]: (![y : A, m : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge' A) cmp ('const/list/NIL' A) (('const/list/CONS' A) y m)) = (('const/list/CONS' A) y m)))).
tt('thm/enumeral/smerge_e3', ax, ![A : $t]: (![y : A, x : A, m : ('type/list/list' A), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge' A) cmp (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)) = (('const/toto/cpn_CASE' ('type/list/list' A)) (('const/toto/apto' A) cmp x y) (('const/list/CONS' A) x (('const/enumeral/smerge' A) cmp l (('const/list/CONS' A) y m))) (('const/list/CONS' A) x (('const/enumeral/smerge' A) cmp l m)) (('const/list/CONS' A) y (('const/enumeral/smerge' A) cmp (('const/list/CONS' A) x l) m)))))).
tt('thm/enumeral/smerge_nil_0', ax, ![A : $t]: (![l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge' A) cmp l ('const/list/NIL' A)) = l))).
tt('thm/enumeral/smerge_nil_e1', ax, ![A : $t]: (![l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge' A) cmp ('const/list/NIL' A) l) = l))).
tt('thm/enumeral/smerge_OL_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A), m : ('type/list/list' A)]: (((('const/enumeral/OL' A) cmp l) & (('const/enumeral/OL' A) cmp m)) => (('const/enumeral/OL' A) cmp (('const/enumeral/smerge' A) cmp l m))))).
tt('thm/enumeral/OL_sublists_tupled_primitive_', def, ![A : $t]: (('const/enumeral/OL_sublists_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) R) & ((![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) cmp lol) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)))) & (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) cmp lol) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)))))))) (^[OL_sublists_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) > $o), a : ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' A)) $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/option/option' ('type/list/list' A)), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/option/option_CASE' ('type/list/list' A) $o) v2 (('const/combin/I' $o) (OL_sublists_tupled (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) cmp lol))) (^[m : ('type/list/list' A)]: (('const/combin/I' $o) ((('const/enumeral/OL' A) cmp m) & (OL_sublists_tupled (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) cmp lol)))))))))))))).
tt('thm/enumeral/OL_sublists_curried_', def, ![A : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((('const/enumeral/OL_sublists' A) x x1) = (('const/enumeral/OL_sublists_tupled' A) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) x x1))))).
tt('thm/enumeral/OL_sublists_ind_', ax, ![A : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' ('type/option/option' ('type/list/list' A))))) & ((![cmp : ('type/toto/toto' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P cmp lol) => (P cmp (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)))) & (![cmp : ('type/toto/toto' A), m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P cmp lol) => (P cmp (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (P v v1))))).
tt('thm/enumeral/OL_sublists_0', ax, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/OL_sublists' A) cmp ('const/list/NIL' ('type/option/option' ('type/list/list' A)))) = $true))).
tt('thm/enumeral/OL_sublists_1', ax, ![A : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), cmp : ('type/toto/toto' A)]: ((('const/enumeral/OL_sublists' A) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)) = (('const/enumeral/OL_sublists' A) cmp lol)))).
tt('thm/enumeral/OL_sublists_e2', ax, ![A : $t]: (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), cmp : ('type/toto/toto' A)]: ((('const/enumeral/OL_sublists' A) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)) = ((('const/enumeral/OL' A) cmp m) & (('const/enumeral/OL_sublists' A) cmp lol))))).
tt('thm/enumeral/lol_set_primitive_', def, ![A : $t]: (('const/enumeral/lol_set' A) = (('const/relation/WFREC' ('type/list/list' ('type/option/option' ('type/list/list' A))) (A > $o)) (('const/min/@' (('type/list/list' ('type/option/option' ('type/list/list' A))) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o))) (^[R : (('type/list/list' ('type/option/option' ('type/list/list' A))) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o))]: ((('const/relation/WF' ('type/list/list' ('type/option/option' ('type/list/list' A)))) R) & ((![lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (R lol (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol))) & (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (R lol (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol))))))) (^[lol_set : (('type/list/list' ('type/option/option' ('type/list/list' A))) > (A > $o)), a : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' A)) (A > $o)) a (('const/combin/I' (A > $o)) ('const/pred_set/EMPTY' A)) (^[v : ('type/option/option' ('type/list/list' A)), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/option/option_CASE' ('type/list/list' A) (A > $o)) v (('const/combin/I' (A > $o)) (lol_set lol)) (^[m : ('type/list/list' A)]: (('const/combin/I' (A > $o)) (('const/pred_set/UNION' A) (('const/list/LIST_TO_SET' A) m) (lol_set lol))))))))))).
tt('thm/enumeral/lol_set_ind_', ax, ![A : $t]: (![P : (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o)]: (((P ('const/list/NIL' ('type/option/option' ('type/list/list' A)))) & ((![lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P lol) => (P (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)))) & (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P lol) => (P (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)))))) => (![v : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (P v))))).
tt('thm/enumeral/lol_set_0', ax, ![A : $t]: ((('const/enumeral/lol_set' A) ('const/list/NIL' ('type/option/option' ('type/list/list' A)))) = ('const/pred_set/EMPTY' A))).
tt('thm/enumeral/lol_set_1', ax, ![A : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((('const/enumeral/lol_set' A) (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)) = (('const/enumeral/lol_set' A) lol)))).
tt('thm/enumeral/lol_set_e2', ax, ![A : $t]: (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((('const/enumeral/lol_set' A) (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)) = (('const/pred_set/UNION' A) (('const/list/LIST_TO_SET' A) m) (('const/enumeral/lol_set' A) lol))))).
tt('thm/enumeral/incr_smerge_tupled_primitive_', def, ![A : $t]: (('const/enumeral/incr_smerge_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))))) R) & (![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), m : ('type/list/list' A), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/enumeral/smerge' A) cmp l m) lol)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)))))))) (^[incr_smerge_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > ('type/list/list' ('type/option/option' ('type/list/list' A)))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/option/option' ('type/list/list' A))) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/option/option' ('type/list/list' A))) ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) v1 (^[l : ('type/list/list' A), v3 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' A)) ('type/list/list' ('type/option/option' ('type/list/list' A)))) v3 (('const/combin/I' ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) l) ('const/list/NIL' ('type/option/option' ('type/list/list' A))))) (^[v4 : ('type/option/option' ('type/list/list' A)), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/option/option_CASE' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) v4 (('const/combin/I' ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) l) lol)) (^[m : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) (incr_smerge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/enumeral/smerge' A) cmp l m) lol))))))))))))))))).
tt('thm/enumeral/incr_smerge_curried_', def, ![A : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' A), x2 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((('const/enumeral/incr_smerge' A) x x1 x2) = (('const/enumeral/incr_smerge_tupled' A) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) x (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) x1 x2)))))).
tt('thm/enumeral/incr_smerge_ind_', ax, ![A : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o)))]: (((![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: (P cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' A))))) & ((![cmp : ('type/toto/toto' A), l : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol))) & (![cmp : ('type/toto/toto' A), l : ('type/list/list' A), m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P cmp (('const/enumeral/smerge' A) cmp l m) lol) => (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' A), v2 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (P v v1 v2))))).
tt('thm/enumeral/incr_smerge_0', ax, ![A : $t]: (![l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/incr_smerge' A) cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' A)))) = (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) l) ('const/list/NIL' ('type/option/option' ('type/list/list' A))))))).
tt('thm/enumeral/incr_smerge_1', ax, ![A : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/incr_smerge' A) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)) = (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) l) lol)))).
tt('thm/enumeral/incr_smerge_e2', ax, ![A : $t]: (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/incr_smerge' A) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)) = (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) (('const/enumeral/incr_smerge' A) cmp (('const/enumeral/smerge' A) cmp l m) lol))))).
tt('thm/enumeral/incr_smerge_OL_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), l : ('type/list/list' A)]: (((('const/enumeral/OL_sublists' A) cmp lol) & (('const/enumeral/OL' A) cmp l)) => (('const/enumeral/OL_sublists' A) cmp (('const/enumeral/incr_smerge' A) cmp l lol))))).
tt('thm/enumeral/smerge_out_tupled_primitive_', def, ![A : $t]: (('const/enumeral/smerge_out_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) ('type/list/list' A)) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))))) R) & ((![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) l lol)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol))))) & (![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), m : ('type/list/list' A), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/enumeral/smerge' A) cmp l m) lol)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol))))))))) (^[smerge_out_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) > ('type/list/list' A)), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) v1 (^[l : ('type/list/list' A), v3 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' A)) ('type/list/list' A)) v3 (('const/combin/I' ('type/list/list' A)) l) (^[v4 : ('type/option/option' ('type/list/list' A)), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (('const/option/option_CASE' ('type/list/list' A) ('type/list/list' A)) v4 (('const/combin/I' ('type/list/list' A)) (smerge_out_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) l lol)))) (^[m : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' A)) (smerge_out_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) (('const/enumeral/smerge' A) cmp l m) lol)))))))))))))))).
tt('thm/enumeral/smerge_out_curried_', def, ![A : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' A), x2 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((('const/enumeral/smerge_out' A) x x1 x2) = (('const/enumeral/smerge_out_tupled' A) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A))))) x (('const/pair/,' ('type/list/list' A) ('type/list/list' ('type/option/option' ('type/list/list' A)))) x1 x2)))))).
tt('thm/enumeral/smerge_out_ind_', ax, ![A : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' ('type/option/option' ('type/list/list' A))) > $o)))]: (((![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: (P cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' A))))) & ((![cmp : ('type/toto/toto' A), l : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P cmp l lol) => (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)))) & (![cmp : ('type/toto/toto' A), l : ('type/list/list' A), m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: ((P cmp (('const/enumeral/smerge' A) cmp l m) lol) => (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' A), v2 : ('type/list/list' ('type/option/option' ('type/list/list' A)))]: (P v v1 v2))))).
tt('thm/enumeral/smerge_out_0', ax, ![A : $t]: (![l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge_out' A) cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' A)))) = l))).
tt('thm/enumeral/smerge_out_1', ax, ![A : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge_out' A) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) ('const/option/NONE' ('type/list/list' A)) lol)) = (('const/enumeral/smerge_out' A) cmp l lol)))).
tt('thm/enumeral/smerge_out_e2', ax, ![A : $t]: (![m : ('type/list/list' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' A))), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/smerge_out' A) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' A))) (('const/option/SOME' ('type/list/list' A)) m) lol)) = (('const/enumeral/smerge_out' A) cmp (('const/enumeral/smerge' A) cmp l m) lol)))).
tt('thm/enumeral/incr_sbuild_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/incr_sbuild' A) cmp ('const/list/NIL' A)) = ('const/list/NIL' ('type/option/option' ('type/list/list' A)))))).
tt('thm/enumeral/incr_sbuild_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A)]: ((('const/enumeral/incr_sbuild' A) cmp (('const/list/CONS' A) x l)) = (('const/enumeral/incr_smerge' A) cmp (('const/list/CONS' A) x ('const/list/NIL' A)) (('const/enumeral/incr_sbuild' A) cmp l))))).
tt('thm/enumeral/incr_ssort_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/enumeral/incr_ssort' A) cmp l) = (('const/enumeral/smerge_out' A) cmp ('const/list/NIL' A) (('const/enumeral/incr_sbuild' A) cmp l))))).
tt('thm/enumeral/bt_to_set_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/ENUMERAL' A) cmp ('const/enumeral/nt' A)) = ('const/pred_set/EMPTY' A)))).
tt('thm/enumeral/bt_to_set_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/enumeral/ENUMERAL' A) cmp (('const/enumeral/node' A) l x r)) = (('const/pred_set/UNION' A) (('const/pred_set/UNION' A) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp l)) & ((('const/toto/apto' A) cmp y x) = 'const/toto/LESS'))))) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) (('const/pred_set/GSPEC' A A) (^[z : A]: (('const/pair/,' A $o) z ((('const/bool/IN' A) z (('const/enumeral/ENUMERAL' A) cmp r)) & ((('const/toto/apto' A) cmp x z) = 'const/toto/LESS'))))))))).
tt('thm/enumeral/bt_to_set_lb_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, t : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_set_lb' A) cmp lb t) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/enumeral/ENUMERAL' A) cmp t)) & ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')))))))).
tt('thm/enumeral/bt_to_set_ub_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A), ub : A]: ((('const/enumeral/bt_to_set_ub' A) cmp t ub) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/enumeral/ENUMERAL' A) cmp t)) & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')))))))).
tt('thm/enumeral/bt_to_set_lb_ub_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, t : ('type/enumeral/bt' A), ub : A]: ((('const/enumeral/bt_to_set_lb_ub' A) cmp lb t ub) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/enumeral/ENUMERAL' A) cmp t)) & (((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS'))))))))).
tt('thm/enumeral/IN_bt_to_set_0', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), y : A]: ((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp ('const/enumeral/nt' A))) = $false))).
tt('thm/enumeral/IN_bt_to_set_e1', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), y : A]: ((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp (('const/enumeral/node' A) l x r))) = (((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp l)) & ((('const/toto/apto' A) cmp y x) = 'const/toto/LESS')) | ((y = x) | ((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp r)) & ((('const/toto/apto' A) cmp x y) = 'const/toto/LESS'))))))).
tt('thm/enumeral/NOT_IN_nt_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), y : A]: ((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp ('const/enumeral/nt' A))) = $false))).
tt('thm/enumeral/IN_node_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), x : A, l : ('type/enumeral/bt' A), y : A, r : ('type/enumeral/bt' A)]: ((('const/bool/IN' A) x (('const/enumeral/ENUMERAL' A) cmp (('const/enumeral/node' A) l y r))) = (('const/toto/cpn_CASE' $o) (('const/toto/apto' A) cmp x y) (('const/bool/IN' A) x (('const/enumeral/ENUMERAL' A) cmp l)) $true (('const/bool/IN' A) x (('const/enumeral/ENUMERAL' A) cmp r)))))).
tt('thm/enumeral/bt_to_ol_lb_ub_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, ub : A]: ((('const/enumeral/bt_to_ol_lb_ub' A) cmp lb ('const/enumeral/nt' A) ub) = ('const/list/NIL' A)))).
tt('thm/enumeral/bt_to_ol_lb_ub_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), ub : A]: ((('const/enumeral/bt_to_ol_lb_ub' A) cmp lb (('const/enumeral/node' A) l x r) ub) = (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/list/APPEND' A) (('const/list/APPEND' A) (('const/enumeral/bt_to_ol_lb_ub' A) cmp lb l x) (('const/list/CONS' A) x ('const/list/NIL' A))) (('const/enumeral/bt_to_ol_lb_ub' A) cmp x r ub)) (('const/enumeral/bt_to_ol_lb_ub' A) cmp lb l ub)) (('const/enumeral/bt_to_ol_lb_ub' A) cmp lb r ub))))).
tt('thm/enumeral/bt_to_ol_lb_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A]: ((('const/enumeral/bt_to_ol_lb' A) cmp lb ('const/enumeral/nt' A)) = ('const/list/NIL' A)))).
tt('thm/enumeral/bt_to_ol_lb_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_ol_lb' A) cmp lb (('const/enumeral/node' A) l x r)) = (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/list/APPEND' A) (('const/list/APPEND' A) (('const/enumeral/bt_to_ol_lb_ub' A) cmp lb l x) (('const/list/CONS' A) x ('const/list/NIL' A))) (('const/enumeral/bt_to_ol_lb' A) cmp x r)) (('const/enumeral/bt_to_ol_lb' A) cmp lb r))))).
tt('thm/enumeral/bt_to_ol_ub_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), ub : A]: ((('const/enumeral/bt_to_ol_ub' A) cmp ('const/enumeral/nt' A) ub) = ('const/list/NIL' A)))).
tt('thm/enumeral/bt_to_ol_ub_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), ub : A]: ((('const/enumeral/bt_to_ol_ub' A) cmp (('const/enumeral/node' A) l x r) ub) = (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/list/APPEND' A) (('const/list/APPEND' A) (('const/enumeral/bt_to_ol_ub' A) cmp l x) (('const/list/CONS' A) x ('const/list/NIL' A))) (('const/enumeral/bt_to_ol_lb_ub' A) cmp x r ub)) (('const/enumeral/bt_to_ol_ub' A) cmp l ub))))).
tt('thm/enumeral/bt_to_ol_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/bt_to_ol' A) cmp ('const/enumeral/nt' A)) = ('const/list/NIL' A)))).
tt('thm/enumeral/bt_to_ol_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_ol' A) cmp (('const/enumeral/node' A) l x r)) = (('const/list/APPEND' A) (('const/list/APPEND' A) (('const/enumeral/bt_to_ol_ub' A) cmp l x) (('const/list/CONS' A) x ('const/list/NIL' A))) (('const/enumeral/bt_to_ol_lb' A) cmp x r))))).
tt('thm/enumeral/ol_set_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A)]: ((('const/enumeral/ENUMERAL' A) cmp t) = (('const/list/LIST_TO_SET' A) (('const/enumeral/bt_to_ol' A) cmp t))))).
tt('thm/enumeral/OL_bt_to_ol_lb_ub_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A), lb : A, ub : A]: (('const/enumeral/OL' A) cmp (('const/enumeral/bt_to_ol_lb_ub' A) cmp lb t ub)))).
tt('thm/enumeral/OL_bt_to_ol_lb_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A), lb : A]: (('const/enumeral/OL' A) cmp (('const/enumeral/bt_to_ol_lb' A) cmp lb t)))).
tt('thm/enumeral/OL_bt_to_ol_ub_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A), ub : A]: (('const/enumeral/OL' A) cmp (('const/enumeral/bt_to_ol_ub' A) cmp t ub)))).
tt('thm/enumeral/OL_bt_to_ol_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A)]: (('const/enumeral/OL' A) cmp (('const/enumeral/bt_to_ol' A) cmp t)))).
tt('thm/enumeral/bt_to_ol_lb_ub_ac_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, ub : A, m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp lb ('const/enumeral/nt' A) ub m) = m))).
tt('thm/enumeral/bt_to_ol_lb_ub_ac_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), ub : A, m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp lb (('const/enumeral/node' A) l x r) ub m) = (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp lb l x (('const/list/CONS' A) x (('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp x r ub m))) (('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp lb l ub m)) (('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp lb r ub m))))).
tt('thm/enumeral/bt_to_ol_lb_ac_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_lb_ac' A) cmp lb ('const/enumeral/nt' A) m) = m))).
tt('thm/enumeral/bt_to_ol_lb_ac_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_lb_ac' A) cmp lb (('const/enumeral/node' A) l x r) m) = (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp lb l x (('const/list/CONS' A) x (('const/enumeral/bt_to_ol_lb_ac' A) cmp x r m))) (('const/enumeral/bt_to_ol_lb_ac' A) cmp lb r m))))).
tt('thm/enumeral/bt_to_ol_ub_ac_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), ub : A, m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_ub_ac' A) cmp ('const/enumeral/nt' A) ub m) = m))).
tt('thm/enumeral/bt_to_ol_ub_ac_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), ub : A, m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_ub_ac' A) cmp (('const/enumeral/node' A) l x r) ub m) = (('const/bool/COND' ('type/list/list' A)) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/enumeral/bt_to_ol_ub_ac' A) cmp l x (('const/list/CONS' A) x (('const/enumeral/bt_to_ol_lb_ub_ac' A) cmp x r ub m))) (('const/enumeral/bt_to_ol_ub_ac' A) cmp l ub m))))).
tt('thm/enumeral/bt_to_ol_ac_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_ac' A) cmp ('const/enumeral/nt' A) m) = m))).
tt('thm/enumeral/bt_to_ol_ac_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), m : ('type/list/list' A)]: ((('const/enumeral/bt_to_ol_ac' A) cmp (('const/enumeral/node' A) l x r) m) = (('const/enumeral/bt_to_ol_ub_ac' A) cmp l x (('const/list/CONS' A) x (('const/enumeral/bt_to_ol_lb_ac' A) cmp x r m)))))).
tt('thm/enumeral/OWL_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), s : (A > $o), l : ('type/list/list' A)]: ((('const/enumeral/OWL' A) cmp s l) = ((s = (('const/list/LIST_TO_SET' A) l)) & (('const/enumeral/OL' A) cmp l))))).
tt('thm/enumeral/OWL_bt_to_ol_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A)]: (('const/enumeral/OWL' A) cmp (('const/enumeral/ENUMERAL' A) cmp t) (('const/enumeral/bt_to_ol' A) cmp t)))).
tt('thm/enumeral/OU_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), t : (A > $o), u : (A > $o)]: ((('const/enumeral/OU' A) cmp t u) = (('const/pred_set/UNION' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x t) & (![z : A]: ((('const/bool/IN' A) z u) => ((('const/toto/apto' A) cmp x z) = 'const/toto/LESS'))))))) u)))).
tt('thm/enumeral/UO_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), s : (A > $o), t : (A > $o)]: ((('const/enumeral/UO' A) cmp s t) = (('const/pred_set/UNION' A) s (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((('const/bool/IN' A) y t) & (![z : A]: ((('const/bool/IN' A) z s) => ((('const/toto/apto' A) cmp z y) = 'const/toto/LESS'))))))))))).
tt('thm/enumeral/EMPTY_OU_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), sl : (A > $o)]: ((('const/enumeral/OU' A) cmp ('const/pred_set/EMPTY' A) sl) = sl))).
tt('thm/enumeral/OU_EMPTY_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : (A > $o)]: ((('const/enumeral/OU' A) cmp t ('const/pred_set/EMPTY' A)) = t))).
tt('thm/enumeral/LESS_UO_LEM_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), x : A, y : A, s : (A > $o)]: ((![z : A]: ((('const/bool/IN' A) z (('const/enumeral/UO' A) cmp (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) s)) => ((('const/toto/apto' A) cmp y z) = 'const/toto/LESS'))) = ((('const/toto/apto' A) cmp y x) = 'const/toto/LESS')))).
tt('thm/enumeral/LESS_ALL_', def, ![A : $t]: (![cmp : ('type/toto/toto' A), x : A, s : (A > $o)]: ((('const/enumeral/LESS_ALL' A) cmp x s) = (![y : A]: ((('const/bool/IN' A) y s) => ((('const/toto/apto' A) cmp x y) = 'const/toto/LESS')))))).
tt('thm/enumeral/LESS_ALL_OU_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), x : A, u : (A > $o), v : (A > $o)]: ((('const/enumeral/LESS_ALL' A) cmp x (('const/enumeral/OU' A) cmp u v)) = ((('const/enumeral/LESS_ALL' A) cmp x u) & (('const/enumeral/LESS_ALL' A) cmp x v))))).
tt('thm/enumeral/OU_ASSOC_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), a : (A > $o), b : (A > $o), c : (A > $o)]: ((('const/enumeral/OU' A) cmp a (('const/enumeral/OU' A) cmp b c)) = (('const/enumeral/OU' A) cmp (('const/enumeral/OU' A) cmp a b) c)))).
tt('thm/enumeral/bl_to_set_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/bl_to_set' A) cmp ('const/enumeral/nbl' A)) = ('const/pred_set/EMPTY' A)))).
tt('thm/enumeral/bl_to_set_1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), b : ('type/enumeral/bl' A)]: ((('const/enumeral/bl_to_set' A) cmp (('const/enumeral/zerbl' A) b)) = (('const/enumeral/bl_to_set' A) cmp b)))).
tt('thm/enumeral/bl_to_set_e2', def, ![A : $t]: (![cmp : ('type/toto/toto' A), x : A, t : ('type/enumeral/bt' A), b : ('type/enumeral/bl' A)]: ((('const/enumeral/bl_to_set' A) cmp (('const/enumeral/onebl' A) x t b)) = (('const/enumeral/OU' A) cmp (('const/pred_set/UNION' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((('const/bool/IN' A) y (('const/enumeral/ENUMERAL' A) cmp t)) & ((('const/toto/apto' A) cmp x y) = 'const/toto/LESS')))))) (('const/enumeral/bl_to_set' A) cmp b))))).
tt('thm/enumeral/LESS_ALL_UO_LEM_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), a : A, s : (A > $o)]: ((('const/enumeral/LESS_ALL' A) cmp a s) => ((('const/enumeral/UO' A) cmp (('const/pred_set/INSERT' A) a ('const/pred_set/EMPTY' A)) s) = (('const/pred_set/INSERT' A) a s))))).
tt('thm/enumeral/LESS_ALL_OU_UO_LEM_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), a : A, s : (A > $o), t : (A > $o)]: (((('const/enumeral/LESS_ALL' A) cmp a s) & (('const/enumeral/LESS_ALL' A) cmp a t)) => ((('const/enumeral/OU' A) cmp (('const/enumeral/UO' A) cmp (('const/pred_set/INSERT' A) a ('const/pred_set/EMPTY' A)) s) t) = (('const/pred_set/INSERT' A) a (('const/enumeral/OU' A) cmp s t)))))).
tt('thm/enumeral/bt_to_ol_ID_IMP_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp l) => ((('const/enumeral/bt_to_ol' A) cmp (('const/enumeral/list_to_bt' A) l)) = l)))).
tt('thm/enumeral/OL_UNION_IMP_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp l) => (![m : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp m) => ((('const/enumeral/OL' A) cmp (('const/enumeral/smerge' A) cmp l m)) & ((('const/list/LIST_TO_SET' A) (('const/enumeral/smerge' A) cmp l m)) = (('const/pred_set/UNION' A) (('const/list/LIST_TO_SET' A) l) (('const/list/LIST_TO_SET' A) m))))))))).
tt('thm/enumeral/sinter_tupled_primitive_', def, ![A : $t]: (('const/enumeral/sinter_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) ('type/list/list' A)) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))) R) & ((![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/EQUAL') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)))))) & ((![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)))))) & (![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l (('const/list/CONS' A) y m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m))))))))))) (^[sinter_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > ('type/list/list' A)), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/list/list' A) ('type/list/list' A)) v1 (^[v2 : ('type/list/list' A), v3 : ('type/list/list' A)]: (('const/list/list_CASE' A ('type/list/list' A)) v2 (('const/combin/I' ('type/list/list' A)) ('const/list/NIL' A)) (^[x : A, l : ('type/list/list' A)]: (('const/list/list_CASE' A ('type/list/list' A)) v3 (('const/combin/I' ('type/list/list' A)) ('const/list/NIL' A)) (^[y : A, m : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' A)) (('const/toto/cpn_CASE' ('type/list/list' A)) (('const/toto/apto' A) cmp x y) (sinter_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l (('const/list/CONS' A) y m)))) (('const/list/CONS' A) x (sinter_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l m)))) (sinter_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) m))))))))))))))))).
tt('thm/enumeral/sinter_curried_', def, ![A : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' A), x2 : ('type/list/list' A)]: ((('const/enumeral/sinter' A) x x1 x2) = (('const/enumeral/sinter_tupled' A) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) x (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) x1 x2)))))).
tt('thm/enumeral/sinter_ind_', ax, ![A : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' A) > $o)))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' A) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A)]: (P cmp (('const/list/CONS' A) x l) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), y : A, m : ('type/list/list' A)]: (P cmp ('const/list/NIL' A) (('const/list/CONS' A) y m))) & (![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A), y : A, m : ('type/list/list' A)]: (((((('const/toto/apto' A) cmp x y) = 'const/toto/EQUAL') => (P cmp l m)) & ((((('const/toto/apto' A) cmp x y) = 'const/toto/GREATER') => (P cmp (('const/list/CONS' A) x l) m)) & (((('const/toto/apto' A) cmp x y) = 'const/toto/LESS') => (P cmp l (('const/list/CONS' A) y m))))) => (P cmp (('const/list/CONS' A) x l) (('const/list/CONS' A) y m))))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' A), v2 : ('type/list/list' A)]: (P v v1 v2))))).
tt('thm/enumeral/sinter_0', ax, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/sinter' A) cmp ('const/list/NIL' A) ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/enumeral/sinter_1', ax, ![A : $t]: (![x : A, l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/sinter' A) cmp (('const/list/CONS' A) x l) ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/enumeral/sinter_2', ax, ![A : $t]: (![y : A, m : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/sinter' A) cmp ('const/list/NIL' A) (('const/list/CONS' A) y m)) = ('const/list/NIL' A)))).
tt('thm/enumeral/sinter_e3', ax, ![A : $t]: (![y : A, x : A, m : ('type/list/list' A), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/sinter' A) cmp (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)) = (('const/toto/cpn_CASE' ('type/list/list' A)) (('const/toto/apto' A) cmp x y) (('const/enumeral/sinter' A) cmp l (('const/list/CONS' A) y m)) (('const/list/CONS' A) x (('const/enumeral/sinter' A) cmp l m)) (('const/enumeral/sinter' A) cmp (('const/list/CONS' A) x l) m))))).
tt('thm/enumeral/OL_INTER_IMP_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp l) => (![m : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp m) => ((('const/enumeral/OL' A) cmp (('const/enumeral/sinter' A) cmp l m)) & ((('const/list/LIST_TO_SET' A) (('const/enumeral/sinter' A) cmp l m)) = (('const/pred_set/INTER' A) (('const/list/LIST_TO_SET' A) l) (('const/list/LIST_TO_SET' A) m))))))))).
tt('thm/enumeral/sdiff_tupled_primitive_', def, ![A : $t]: (('const/enumeral/sdiff_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) ('type/list/list' A)) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))) R) & ((![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/EQUAL') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)))))) & ((![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)))))) & (![m : ('type/list/list' A), l : ('type/list/list' A), y : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x y) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l (('const/list/CONS' A) y m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) (('const/list/CONS' A) y m))))))))))) (^[sdiff_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) > ('type/list/list' A)), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/list/list' A) ('type/list/list' A)) v1 (^[v2 : ('type/list/list' A), v3 : ('type/list/list' A)]: (('const/list/list_CASE' A ('type/list/list' A)) v2 (('const/combin/I' ('type/list/list' A)) ('const/list/NIL' A)) (^[x : A, l : ('type/list/list' A)]: (('const/list/list_CASE' A ('type/list/list' A)) v3 (('const/combin/I' ('type/list/list' A)) (('const/list/CONS' A) x l)) (^[y : A, m : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' A)) (('const/toto/cpn_CASE' ('type/list/list' A)) (('const/toto/apto' A) cmp x y) (('const/list/CONS' A) x (sdiff_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l (('const/list/CONS' A) y m))))) (sdiff_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l m))) (sdiff_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x l) m))))))))))))))))).
tt('thm/enumeral/sdiff_curried_', def, ![A : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' A), x2 : ('type/list/list' A)]: ((('const/enumeral/sdiff' A) x x1 x2) = (('const/enumeral/sdiff_tupled' A) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) x (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) x1 x2)))))).
tt('thm/enumeral/sdiff_ind_', ax, ![A : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' A) > (('type/list/list' A) > $o)))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' A) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A)]: (P cmp (('const/list/CONS' A) x l) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), y : A, m : ('type/list/list' A)]: (P cmp ('const/list/NIL' A) (('const/list/CONS' A) y m))) & (![cmp : ('type/toto/toto' A), x : A, l : ('type/list/list' A), y : A, m : ('type/list/list' A)]: (((((('const/toto/apto' A) cmp x y) = 'const/toto/EQUAL') => (P cmp l m)) & ((((('const/toto/apto' A) cmp x y) = 'const/toto/GREATER') => (P cmp (('const/list/CONS' A) x l) m)) & (((('const/toto/apto' A) cmp x y) = 'const/toto/LESS') => (P cmp l (('const/list/CONS' A) y m))))) => (P cmp (('const/list/CONS' A) x l) (('const/list/CONS' A) y m))))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' A), v2 : ('type/list/list' A)]: (P v v1 v2))))).
tt('thm/enumeral/sdiff_0', ax, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/sdiff' A) cmp ('const/list/NIL' A) ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/enumeral/sdiff_1', ax, ![A : $t]: (![x : A, l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/sdiff' A) cmp (('const/list/CONS' A) x l) ('const/list/NIL' A)) = (('const/list/CONS' A) x l)))).
tt('thm/enumeral/sdiff_2', ax, ![A : $t]: (![y : A, m : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/sdiff' A) cmp ('const/list/NIL' A) (('const/list/CONS' A) y m)) = ('const/list/NIL' A)))).
tt('thm/enumeral/sdiff_e3', ax, ![A : $t]: (![y : A, x : A, m : ('type/list/list' A), l : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/enumeral/sdiff' A) cmp (('const/list/CONS' A) x l) (('const/list/CONS' A) y m)) = (('const/toto/cpn_CASE' ('type/list/list' A)) (('const/toto/apto' A) cmp x y) (('const/list/CONS' A) x (('const/enumeral/sdiff' A) cmp l (('const/list/CONS' A) y m))) (('const/enumeral/sdiff' A) cmp l m) (('const/enumeral/sdiff' A) cmp (('const/list/CONS' A) x l) m))))).
tt('thm/enumeral/OL_DIFF_IMP_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp l) => (![m : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp m) => ((('const/enumeral/OL' A) cmp (('const/enumeral/sdiff' A) cmp l m)) & ((('const/list/LIST_TO_SET' A) (('const/enumeral/sdiff' A) cmp l m)) = (('const/pred_set/DIFF' A) (('const/list/LIST_TO_SET' A) l) (('const/list/LIST_TO_SET' A) m))))))))).
tt('thm/enumeral/ENUMERAL_set_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/list/LIST_TO_SET' A) l) = (('const/enumeral/ENUMERAL' A) cmp (('const/enumeral/list_to_bt' A) (('const/enumeral/incr_ssort' A) cmp l)))))).
tt('thm/enumeral/OL_ENUMERAL_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp l) => ((('const/list/LIST_TO_SET' A) l) = (('const/enumeral/ENUMERAL' A) cmp (('const/enumeral/list_to_bt' A) l)))))).
tt('thm/enumeral/OWL_UNION_THM_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), s : (A > $o), l : ('type/list/list' A), t : (A > $o), m : ('type/list/list' A)]: (((('const/enumeral/OWL' A) cmp s l) & (('const/enumeral/OWL' A) cmp t m)) => (('const/enumeral/OWL' A) cmp (('const/pred_set/UNION' A) s t) (('const/enumeral/smerge' A) cmp l m))))).
tt('thm/enumeral/OWL_INTER_THM_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), s : (A > $o), l : ('type/list/list' A), t : (A > $o), m : ('type/list/list' A)]: (((('const/enumeral/OWL' A) cmp s l) & (('const/enumeral/OWL' A) cmp t m)) => (('const/enumeral/OWL' A) cmp (('const/pred_set/INTER' A) s t) (('const/enumeral/sinter' A) cmp l m))))).
tt('thm/enumeral/OWL_DIFF_THM_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), s : (A > $o), l : ('type/list/list' A), t : (A > $o), m : ('type/list/list' A)]: (((('const/enumeral/OWL' A) cmp s l) & (('const/enumeral/OWL' A) cmp t m)) => (('const/enumeral/OWL' A) cmp (('const/pred_set/DIFF' A) s t) (('const/enumeral/sdiff' A) cmp l m))))).
tt('thm/enumeral/OL_bt_lb_ub_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, ub : A]: ((('const/enumeral/OL_bt_lb_ub' A) cmp lb ('const/enumeral/nt' A) ub) = ((('const/toto/apto' A) cmp lb ub) = 'const/toto/LESS')))).
tt('thm/enumeral/OL_bt_lb_ub_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), ub : A]: ((('const/enumeral/OL_bt_lb_ub' A) cmp lb (('const/enumeral/node' A) l x r) ub) = ((('const/enumeral/OL_bt_lb_ub' A) cmp lb l x) & (('const/enumeral/OL_bt_lb_ub' A) cmp x r ub))))).
tt('thm/enumeral/OL_bt_lb_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A]: ((('const/enumeral/OL_bt_lb' A) cmp lb ('const/enumeral/nt' A)) = $true))).
tt('thm/enumeral/OL_bt_lb_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/enumeral/OL_bt_lb' A) cmp lb (('const/enumeral/node' A) l x r)) = ((('const/enumeral/OL_bt_lb_ub' A) cmp lb l x) & (('const/enumeral/OL_bt_lb' A) cmp x r))))).
tt('thm/enumeral/OL_bt_ub_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A), ub : A]: ((('const/enumeral/OL_bt_ub' A) cmp ('const/enumeral/nt' A) ub) = $true))).
tt('thm/enumeral/OL_bt_ub_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A), ub : A]: ((('const/enumeral/OL_bt_ub' A) cmp (('const/enumeral/node' A) l x r) ub) = ((('const/enumeral/OL_bt_ub' A) cmp l x) & (('const/enumeral/OL_bt_lb_ub' A) cmp x r ub))))).
tt('thm/enumeral/OL_bt_0', def, ![A : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/enumeral/OL_bt' A) cmp ('const/enumeral/nt' A)) = $true))).
tt('thm/enumeral/OL_bt_e1', def, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/enumeral/OL_bt' A) cmp (('const/enumeral/node' A) l x r)) = ((('const/enumeral/OL_bt_ub' A) cmp l x) & (('const/enumeral/OL_bt_lb' A) cmp x r))))).
tt('thm/enumeral/better_bt_to_ol_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' A)]: ((('const/enumeral/bt_to_ol' A) cmp t) = (('const/bool/COND' ('type/list/list' A)) (('const/enumeral/OL_bt' A) cmp t) (('const/enumeral/bt_to_list_ac' A) t ('const/list/NIL' A)) (('const/enumeral/bt_to_ol_ac' A) cmp t ('const/list/NIL' A)))))).
tt('thm/enumeral/set_OWL_thm_', ax, ![A : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' A)]: (('const/enumeral/OWL' A) cmp (('const/list/LIST_TO_SET' A) l) (('const/enumeral/incr_ssort' A) cmp l)))).
