tt('const/rich_list/AND_EL', ty, (('type/list/list' $o) > $o)).
tt('const/rich_list/BUTLASTN', ty, ![A : $t]: ('type/num/num' > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/rich_list/COUNT_LIST', ty, ('type/num/num' > ('type/list/list' 'type/num/num'))).
tt('const/rich_list/COUNT_LIST_AUX', ty, ('type/num/num' > (('type/list/list' 'type/num/num') > ('type/list/list' 'type/num/num')))).
tt('const/rich_list/ELL', ty, ![A : $t]: ('type/num/num' > (('type/list/list' A) > A))).
tt('const/rich_list/IS_SUBLIST', ty, ![A : $t]: (('type/list/list' A) > (('type/list/list' A) > $o))).
tt('const/rich_list/IS_SUFFIX', ty, ![A : $t]: (('type/list/list' A) > (('type/list/list' A) > $o))).
tt('const/rich_list/LASTN', ty, ![A : $t]: ('type/num/num' > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/rich_list/LIST_ELEM_COUNT', ty, ![A : $t]: (A > (('type/list/list' A) > 'type/num/num'))).
tt('const/rich_list/OR_EL', ty, (('type/list/list' $o) > $o)).
tt('const/rich_list/PREFIX', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/rich_list/REPLICATE', ty, ![A : $t]: ('type/num/num' > (A > ('type/list/list' A)))).
tt('const/rich_list/SCANL', ty, ![A : $t, B : $t]: ((B > (A > B)) > (B > (('type/list/list' A) > ('type/list/list' B))))).
tt('const/rich_list/SCANR', ty, ![A : $t, B : $t]: ((A > (B > B)) > (B > (('type/list/list' A) > ('type/list/list' B))))).
tt('const/rich_list/SEG', ty, ![A : $t]: ('type/num/num' > ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/rich_list/SPLITL', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))))).
tt('const/rich_list/SPLITP', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))))).
tt('const/rich_list/SPLITP_AUX', ty, ![A : $t]: (('type/list/list' A) > ((A > $o) > (('type/list/list' A) > ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)))))).
tt('const/rich_list/SPLITR', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))))).
tt('const/rich_list/SUFFIX', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/rich_list/UNZIP_FST', ty, ![A : $t, B : $t]: (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' A))).
tt('const/rich_list/UNZIP_SND', ty, ![A : $t, B : $t]: (('type/list/list' ('type/pair/prod' B A)) > ('type/list/list' A))).
tt('thm/rich_list/ELL_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) 'const/num/0' l) = (('const/list/LAST' A) l)))).
tt('thm/rich_list/ELL_e1', def, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) ('const/num/SUC' n) l) = (('const/rich_list/ELL' A) n (('const/list/FRONT' A) l))))).
tt('thm/rich_list/ELL_compute_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) 'const/num/0' l) = (('const/list/LAST' A) l)))).
tt('thm/rich_list/ELL_compute_1', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) l) = (('const/rich_list/ELL' A) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/list/FRONT' A) l))))).
tt('thm/rich_list/ELL_compute_e2', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) l) = (('const/rich_list/ELL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/FRONT' A) l))))).
tt('thm/rich_list/REPLICATE_0', def, ![A : $t]: (![x : A]: ((('const/rich_list/REPLICATE' A) 'const/num/0' x) = ('const/list/NIL' A)))).
tt('thm/rich_list/REPLICATE_e1', def, ![A : $t]: (![n : 'type/num/num', x : A]: ((('const/rich_list/REPLICATE' A) ('const/num/SUC' n) x) = (('const/list/CONS' A) x (('const/rich_list/REPLICATE' A) n x))))).
tt('thm/rich_list/REPLICATE_compute_0', ax, ![A : $t]: (![x : A]: ((('const/rich_list/REPLICATE' A) 'const/num/0' x) = ('const/list/NIL' A)))).
tt('thm/rich_list/REPLICATE_compute_1', ax, ![A : $t]: (![n : 'type/num/num', x : A]: ((('const/rich_list/REPLICATE' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) x) = (('const/list/CONS' A) x (('const/rich_list/REPLICATE' A) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x))))).
tt('thm/rich_list/REPLICATE_compute_e2', ax, ![A : $t]: (![n : 'type/num/num', x : A]: ((('const/rich_list/REPLICATE' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) x) = (('const/list/CONS' A) x (('const/rich_list/REPLICATE' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) x))))).
tt('thm/rich_list/SCANL_0', def, ![B : $t, A : $t]: (![f : (B > (A > B)), e : B]: ((('const/rich_list/SCANL' A B) f e ('const/list/NIL' A)) = (('const/list/CONS' B) e ('const/list/NIL' B))))).
tt('thm/rich_list/SCANL_e1', def, ![A : $t, B : $t]: (![f : (B > (A > B)), e : B, x : A, l : ('type/list/list' A)]: ((('const/rich_list/SCANL' A B) f e (('const/list/CONS' A) x l)) = (('const/list/CONS' B) e (('const/rich_list/SCANL' A B) f (f e x) l))))).
tt('thm/rich_list/SCANR_0', def, ![B : $t, A : $t]: (![f : (A > (B > B)), e : B]: ((('const/rich_list/SCANR' A B) f e ('const/list/NIL' A)) = (('const/list/CONS' B) e ('const/list/NIL' B))))).
tt('thm/rich_list/SCANR_e1', def, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, x : A, l : ('type/list/list' A)]: ((('const/rich_list/SCANR' A B) f e (('const/list/CONS' A) x l)) = (('const/list/CONS' B) (f x (('const/list/HD' B) (('const/rich_list/SCANR' A B) f e l))) (('const/rich_list/SCANR' A B) f e l))))).
tt('thm/rich_list/SPLITP_0', def, ![A : $t]: (![P : (A > $o)]: ((('const/rich_list/SPLITP' A) P ('const/list/NIL' A)) = (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) ('const/list/NIL' A) ('const/list/NIL' A))))).
tt('thm/rich_list/SPLITP_e1', def, ![A : $t]: (![P : (A > $o), x : A, l : ('type/list/list' A)]: ((('const/rich_list/SPLITP' A) P (('const/list/CONS' A) x l)) = (('const/bool/COND' ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) (P x) (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) ('const/list/NIL' A) (('const/list/CONS' A) x l)) (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/CONS' A) x (('const/pair/FST' ('type/list/list' A) ('type/list/list' A)) (('const/rich_list/SPLITP' A) P l))) (('const/pair/SND' ('type/list/list' A) ('type/list/list' A)) (('const/rich_list/SPLITP' A) P l))))))).
tt('thm/rich_list/SPLITP_AUX_def_0', def, ![A : $t]: (![acc : ('type/list/list' A), P : (A > $o)]: ((('const/rich_list/SPLITP_AUX' A) acc P ('const/list/NIL' A)) = (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) acc ('const/list/NIL' A))))).
tt('thm/rich_list/SPLITP_AUX_def_e1', def, ![A : $t]: (![acc : ('type/list/list' A), P : (A > $o), h : A, t : ('type/list/list' A)]: ((('const/rich_list/SPLITP_AUX' A) acc P (('const/list/CONS' A) h t)) = (('const/bool/COND' ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) (P h) (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) acc (('const/list/CONS' A) h t)) (('const/rich_list/SPLITP_AUX' A) (('const/list/APPEND' A) acc (('const/list/CONS' A) h ('const/list/NIL' A))) P t))))).
tt('thm/rich_list/SPLITL_def_', def, ![A : $t]: (![P : (A > $o)]: ((('const/rich_list/SPLITL' A) P) = (('const/rich_list/SPLITP' A) (('const/combin/o' A $o $o) $not P))))).
tt('thm/rich_list/SPLITR_def_', def, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/rich_list/SPLITR' A) P l) = (('const/bool/LET' ('type/pair/prod' ('type/list/list' A) ('type/list/list' A)) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) (('const/pair/UNCURRY' ('type/list/list' A) ('type/list/list' A) ('type/pair/prod' ('type/list/list' A) ('type/list/list' A))) (^[a : ('type/list/list' A), b : ('type/list/list' A)]: (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) (('const/list/REVERSE' A) b) (('const/list/REVERSE' A) a)))) (('const/rich_list/SPLITP' A) (('const/combin/o' A $o $o) $not P) (('const/list/REVERSE' A) l)))))).
tt('thm/rich_list/PREFIX_DEF_', def, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/rich_list/PREFIX' A) P l) = (('const/pair/FST' ('type/list/list' A) ('type/list/list' A)) (('const/rich_list/SPLITP' A) (('const/combin/o' A $o $o) $not P) l))))).
tt('thm/rich_list/SUFFIX_DEF_', def, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/rich_list/SUFFIX' A) P l) = (('const/list/FOLDL' A ('type/list/list' A)) (^['l\'' : ('type/list/list' A), x : A]: (('const/bool/COND' ('type/list/list' A)) (P x) (('const/list/SNOC' A) x 'l\'') ('const/list/NIL' A))) ('const/list/NIL' A) l)))).
tt('thm/rich_list/AND_EL_DEF_', def, ('const/rich_list/AND_EL' = (('const/list/EVERY' $o) ('const/combin/I' $o)))).
tt('thm/rich_list/OR_EL_DEF_', def, ('const/rich_list/OR_EL' = (('const/list/EXISTS' $o) ('const/combin/I' $o)))).
tt('thm/rich_list/UNZIP_FST_DEF_', def, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/rich_list/UNZIP_FST' A B) l) = (('const/pair/FST' ('type/list/list' A) ('type/list/list' B)) (('const/list/UNZIP' A B) l))))).
tt('thm/rich_list/UNZIP_SND_DEF_', def, ![B : $t, A : $t]: (![l : ('type/list/list' ('type/pair/prod' B A))]: ((('const/rich_list/UNZIP_SND' A B) l) = (('const/pair/SND' ('type/list/list' B) ('type/list/list' A)) (('const/list/UNZIP' B A) l))))).
tt('thm/rich_list/LIST_ELEM_COUNT_DEF_', def, ![A : $t]: (![e : A, l : ('type/list/list' A)]: ((('const/rich_list/LIST_ELEM_COUNT' A) e l) = (('const/list/LENGTH' A) (('const/list/FILTER' A) (^[x : A]: (x = e)) l))))).
tt('thm/rich_list/COUNT_LIST_def_0', def, (('const/rich_list/COUNT_LIST' 'const/num/0') = ('const/list/NIL' 'type/num/num'))).
tt('thm/rich_list/COUNT_LIST_def_e1', def, (![n : 'type/num/num']: (('const/rich_list/COUNT_LIST' ('const/num/SUC' n)) = (('const/list/CONS' 'type/num/num') 'const/num/0' (('const/list/MAP' 'type/num/num' 'type/num/num') 'const/num/SUC' ('const/rich_list/COUNT_LIST' n)))))).
tt('thm/rich_list/COUNT_LIST_AUX_def_0', def, (![l : ('type/list/list' 'type/num/num')]: (('const/rich_list/COUNT_LIST_AUX' 'const/num/0' l) = l))).
tt('thm/rich_list/COUNT_LIST_AUX_def_e1', def, (![n : 'type/num/num', l : ('type/list/list' 'type/num/num')]: (('const/rich_list/COUNT_LIST_AUX' ('const/num/SUC' n) l) = ('const/rich_list/COUNT_LIST_AUX' n (('const/list/CONS' 'type/num/num') n l))))).
tt('thm/rich_list/COUNT_LIST_AUX_def_compute_0', ax, (![l : ('type/list/list' 'type/num/num')]: (('const/rich_list/COUNT_LIST_AUX' 'const/num/0' l) = l))).
tt('thm/rich_list/COUNT_LIST_AUX_def_compute_1', ax, (![n : 'type/num/num', l : ('type/list/list' 'type/num/num')]: (('const/rich_list/COUNT_LIST_AUX' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) l) = ('const/rich_list/COUNT_LIST_AUX' ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/list/CONS' 'type/num/num') ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) l))))).
tt('thm/rich_list/COUNT_LIST_AUX_def_compute_e2', ax, (![n : 'type/num/num', l : ('type/list/list' 'type/num/num')]: (('const/rich_list/COUNT_LIST_AUX' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) l) = ('const/rich_list/COUNT_LIST_AUX' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/CONS' 'type/num/num') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) l))))).
tt('thm/rich_list/TAKE_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/TAKE' A) 'const/num/0' l) = ('const/list/NIL' A)))).
tt('thm/rich_list/TAKE_e1', ax, ![A : $t]: (![n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/list/TAKE' A) ('const/num/SUC' n) (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/list/TAKE' A) n l))))).
tt('thm/rich_list/DROP_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/DROP' A) 'const/num/0' l) = l))).
tt('thm/rich_list/DROP_e1', ax, ![A : $t]: (![n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/list/DROP' A) ('const/num/SUC' n) (('const/list/CONS' A) x l)) = (('const/list/DROP' A) n l)))).
tt('thm/rich_list/NOT_NULL_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: (~ (('const/list/NULL' A) (('const/list/SNOC' A) x l))))).
tt('thm/rich_list/LASTN_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) 'const/num/0' l) = ('const/list/NIL' A)))).
tt('thm/rich_list/LASTN_e1', def, ![A : $t]: (![n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) ('const/num/SUC' n) (('const/list/SNOC' A) x l)) = (('const/list/SNOC' A) x (('const/rich_list/LASTN' A) n l))))).
tt('thm/rich_list/BUTLASTN_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/BUTLASTN' A) 'const/num/0' l) = l))).
tt('thm/rich_list/BUTLASTN_e1', def, ![A : $t]: (![n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/BUTLASTN' A) ('const/num/SUC' n) (('const/list/SNOC' A) x l)) = (('const/rich_list/BUTLASTN' A) n l)))).
tt('thm/rich_list/IS_SUBLIST_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/IS_SUBLIST' A) l ('const/list/NIL' A)) = $true))).
tt('thm/rich_list/IS_SUBLIST_1', def, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/rich_list/IS_SUBLIST' A) ('const/list/NIL' A) (('const/list/CONS' A) x l)) = $false))).
tt('thm/rich_list/IS_SUBLIST_e2', def, ![A : $t]: (![x1 : A, l1 : ('type/list/list' A), x2 : A, l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUBLIST' A) (('const/list/CONS' A) x1 l1) (('const/list/CONS' A) x2 l2)) = (((x1 = x2) & (('const/list/isPREFIX' A) l2 l1)) | (('const/rich_list/IS_SUBLIST' A) l1 (('const/list/CONS' A) x2 l2)))))).
tt('thm/rich_list/SEG_0', def, ![A : $t]: (![k : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) 'const/num/0' k l) = ('const/list/NIL' A)))).
tt('thm/rich_list/SEG_1', def, ![A : $t]: (![m : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/num/SUC' m) 'const/num/0' (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/rich_list/SEG' A) m 'const/num/0' l))))).
tt('thm/rich_list/SEG_e2', def, ![A : $t]: (![m : 'type/num/num', k : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/num/SUC' m) ('const/num/SUC' k) (('const/list/CONS' A) x l)) = (('const/rich_list/SEG' A) ('const/num/SUC' m) k l)))).
tt('thm/rich_list/IS_SUFFIX_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) l ('const/list/NIL' A)) = $true))).
tt('thm/rich_list/IS_SUFFIX_1', def, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) ('const/list/NIL' A) (('const/list/SNOC' A) x l)) = $false))).
tt('thm/rich_list/IS_SUFFIX_e2', def, ![A : $t]: (![x1 : A, l1 : ('type/list/list' A), x2 : A, l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) (('const/list/SNOC' A) x1 l1) (('const/list/SNOC' A) x2 l2)) = ((x1 = x2) & (('const/rich_list/IS_SUFFIX' A) l1 l2))))).
tt('thm/rich_list/LENGTH_MAP2_', ax, ![B : $t, A : $t, C : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => (![f : (A > (B > C))]: (((('const/list/LENGTH' C) (('const/list/MAP2' C A B) f l1 l2)) = (('const/list/LENGTH' A) l1)) & ((('const/list/LENGTH' C) (('const/list/MAP2' C A B) f l1 l2)) = (('const/list/LENGTH' B) l2))))))).
tt('thm/rich_list/LENGTH_EQ_', ax, ![A : $t]: (![x : ('type/list/list' A), y : ('type/list/list' A)]: ((x = y) => ((('const/list/LENGTH' A) x) = (('const/list/LENGTH' A) y))))).
tt('thm/rich_list/LENGTH_NOT_NULL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (('const/prim_rec/<' 'const/num/0' (('const/list/LENGTH' A) l)) = (~ (('const/list/NULL' A) l))))).
tt('thm/rich_list/NOT_NIL_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: (~ (('const/list/NIL' A) = (('const/list/SNOC' A) x l))))).
tt('thm/rich_list/NOT_SNOC_NIL_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: (~ ((('const/list/SNOC' A) x l) = ('const/list/NIL' A))))).
tt('thm/rich_list/SNOC_EQ_LENGTH_EQ_', ax, ![A : $t]: (![x1 : A, l1 : ('type/list/list' A), x2 : A, l2 : ('type/list/list' A)]: (((('const/list/SNOC' A) x1 l1) = (('const/list/SNOC' A) x2 l2)) => ((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' A) l2))))).
tt('thm/rich_list/SNOC_REVERSE_CONS_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/SNOC' A) x l) = (('const/list/REVERSE' A) (('const/list/CONS' A) x (('const/list/REVERSE' A) l)))))).
tt('thm/rich_list/FOLDR_SNOC_', ax, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, x : A, l : ('type/list/list' A)]: ((('const/list/FOLDR' A B) f e (('const/list/SNOC' A) x l)) = (('const/list/FOLDR' A B) f (f x e) l)))).
tt('thm/rich_list/FOLDR_FOLDL_', ax, ![A : $t]: (![f : (A > (A > A)), e : A]: ((('const/operator/MONOID' A) f e) => (![l : ('type/list/list' A)]: ((('const/list/FOLDR' A A) f e l) = (('const/list/FOLDL' A A) f e l)))))).
tt('thm/rich_list/LENGTH_FOLDR_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/LENGTH' A) l) = (('const/list/FOLDR' A 'type/num/num') (^[x : A, 'l\'' : 'type/num/num']: ('const/num/SUC' 'l\'')) 'const/num/0' l)))).
tt('thm/rich_list/LENGTH_FOLDL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/LENGTH' A) l) = (('const/list/FOLDL' A 'type/num/num') (^['l\'' : 'type/num/num', x : A]: ('const/num/SUC' 'l\'')) 'const/num/0' l)))).
tt('thm/rich_list/MAP_FOLDR_', ax, ![A : $t, B : $t]: (![f : (A > B), l : ('type/list/list' A)]: ((('const/list/MAP' A B) f l) = (('const/list/FOLDR' A ('type/list/list' B)) (^[x : A, 'l\'' : ('type/list/list' B)]: (('const/list/CONS' B) (f x) 'l\'')) ('const/list/NIL' B) l)))).
tt('thm/rich_list/MAP_FOLDL_', ax, ![A : $t, B : $t]: (![f : (A > B), l : ('type/list/list' A)]: ((('const/list/MAP' A B) f l) = (('const/list/FOLDL' A ('type/list/list' B)) (^['l\'' : ('type/list/list' B), x : A]: (('const/list/SNOC' B) (f x) 'l\'')) ('const/list/NIL' B) l)))).
tt('thm/rich_list/FILTER_FOLDR_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/FILTER' A) P l) = (('const/list/FOLDR' A ('type/list/list' A)) (^[x : A, 'l\'' : ('type/list/list' A)]: (('const/bool/COND' ('type/list/list' A)) (P x) (('const/list/CONS' A) x 'l\'') 'l\'')) ('const/list/NIL' A) l)))).
tt('thm/rich_list/FILTER_SNOC_', ax, ![A : $t]: (![P : (A > $o), x : A, l : ('type/list/list' A)]: ((('const/list/FILTER' A) P (('const/list/SNOC' A) x l)) = (('const/bool/COND' ('type/list/list' A)) (P x) (('const/list/SNOC' A) x (('const/list/FILTER' A) P l)) (('const/list/FILTER' A) P l))))).
tt('thm/rich_list/FILTER_FOLDL_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/FILTER' A) P l) = (('const/list/FOLDL' A ('type/list/list' A)) (^['l\'' : ('type/list/list' A), x : A]: (('const/bool/COND' ('type/list/list' A)) (P x) (('const/list/SNOC' A) x 'l\'') 'l\'')) ('const/list/NIL' A) l)))).
tt('thm/rich_list/FILTER_COMM_', ax, ![A : $t]: (![f1 : (A > $o), f2 : (A > $o), l : ('type/list/list' A)]: ((('const/list/FILTER' A) f1 (('const/list/FILTER' A) f2 l)) = (('const/list/FILTER' A) f2 (('const/list/FILTER' A) f1 l))))).
tt('thm/rich_list/FILTER_IDEM_', ax, ![A : $t]: (![f : (A > $o), l : ('type/list/list' A)]: ((('const/list/FILTER' A) f (('const/list/FILTER' A) f l)) = (('const/list/FILTER' A) f l)))).
tt('thm/rich_list/FILTER_MAP_', ax, ![B : $t, A : $t]: (![f1 : (A > $o), f2 : (B > A), l : ('type/list/list' B)]: ((('const/list/FILTER' A) f1 (('const/list/MAP' B A) f2 l)) = (('const/list/MAP' B A) f2 (('const/list/FILTER' B) (('const/combin/o' B $o A) f1 f2) l))))).
tt('thm/rich_list/LENGTH_FILTER_LEQ_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ('const/arithmetic/<=' (('const/list/LENGTH' A) (('const/list/FILTER' A) P l)) (('const/list/LENGTH' A) l)))).
tt('thm/rich_list/FILTER_EQ_', ax, ![A : $t]: (![P1 : (A > $o), P2 : (A > $o), l : ('type/list/list' A)]: (((('const/list/FILTER' A) P1 l) = (('const/list/FILTER' A) P2 l)) = (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) => ((P1 x) = (P2 x))))))).
tt('thm/rich_list/LENGTH_SEG_', ax, ![A : $t]: (![n : 'type/num/num', k : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n k) (('const/list/LENGTH' A) l)) => ((('const/list/LENGTH' A) (('const/rich_list/SEG' A) n k l)) = n)))).
tt('thm/rich_list/APPEND_NIL_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/APPEND' A) l ('const/list/NIL' A)) = l))).
tt('thm/rich_list/APPEND_NIL_e1', ax, ![B : $t]: (![l : ('type/list/list' B)]: ((('const/list/APPEND' B) ('const/list/NIL' B) l) = l))).
tt('thm/rich_list/APPEND_FOLDR_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/APPEND' A) l1 l2) = (('const/list/FOLDR' A ('type/list/list' A)) ('const/list/CONS' A) l2 l1)))).
tt('thm/rich_list/APPEND_FOLDL_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/APPEND' A) l1 l2) = (('const/list/FOLDL' A ('type/list/list' A)) (^['l\'' : ('type/list/list' A), x : A]: (('const/list/SNOC' A) x 'l\'')) l1 l2)))).
tt('thm/rich_list/FOLDR_APPEND_', ax, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/FOLDR' A B) f e (('const/list/APPEND' A) l1 l2)) = (('const/list/FOLDR' A B) f (('const/list/FOLDR' A B) f e l2) l1)))).
tt('thm/rich_list/FOLDL_APPEND_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), e : A, l1 : ('type/list/list' B), l2 : ('type/list/list' B)]: ((('const/list/FOLDL' B A) f e (('const/list/APPEND' B) l1 l2)) = (('const/list/FOLDL' B A) f (('const/list/FOLDL' B A) f e l1) l2)))).
tt('thm/rich_list/CONS_APPEND_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/CONS' A) x l) = (('const/list/APPEND' A) (('const/list/CONS' A) x ('const/list/NIL' A)) l)))).
tt('thm/rich_list/ASSOC_APPEND_', ax, ![A : $t]: (('const/operator/ASSOC' ('type/list/list' A)) ('const/list/APPEND' A))).
tt('thm/rich_list/MONOID_APPEND_NIL_', ax, ![A : $t]: (('const/operator/MONOID' ('type/list/list' A)) ('const/list/APPEND' A) ('const/list/NIL' A))).
tt('thm/rich_list/FLAT_SNOC_', ax, ![A : $t]: (![x : ('type/list/list' A), l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FLAT' A) (('const/list/SNOC' ('type/list/list' A)) x l)) = (('const/list/APPEND' A) (('const/list/FLAT' A) l) x)))).
tt('thm/rich_list/FLAT_FOLDR_', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FLAT' A) l) = (('const/list/FOLDR' ('type/list/list' A) ('type/list/list' A)) ('const/list/APPEND' A) ('const/list/NIL' A) l)))).
tt('thm/rich_list/FLAT_FOLDL_', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FLAT' A) l) = (('const/list/FOLDL' ('type/list/list' A) ('type/list/list' A)) ('const/list/APPEND' A) ('const/list/NIL' A) l)))).
tt('thm/rich_list/LENGTH_FLAT_', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/LENGTH' A) (('const/list/FLAT' A) l)) = ('const/list/SUM' (('const/list/MAP' ('type/list/list' A) 'type/num/num') ('const/list/LENGTH' A) l))))).
tt('thm/rich_list/REVERSE_FOLDR_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/REVERSE' A) l) = (('const/list/FOLDR' A ('type/list/list' A)) ('const/list/SNOC' A) ('const/list/NIL' A) l)))).
tt('thm/rich_list/REVERSE_FOLDL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/REVERSE' A) l) = (('const/list/FOLDL' A ('type/list/list' A)) (^['l\'' : ('type/list/list' A), x : A]: (('const/list/CONS' A) x 'l\'')) ('const/list/NIL' A) l)))).
tt('thm/rich_list/ALL_EL_MAP_', ax, ![B : $t, A : $t]: (![P : (A > $o), f : (B > A), l : ('type/list/list' B)]: ((('const/list/EVERY' A) P (('const/list/MAP' B A) f l)) = (('const/list/EVERY' B) (('const/combin/o' B $o A) P f) l)))).
tt('thm/rich_list/MEM_EXISTS_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) = (('const/list/EXISTS' A) (($equals A) x) l)))).
tt('thm/rich_list/SUM_FOLDR_', ax, (![l : ('type/list/list' 'type/num/num')]: (('const/list/SUM' l) = (('const/list/FOLDR' 'type/num/num' 'type/num/num') 'const/arithmetic/+' 'const/num/0' l)))).
tt('thm/rich_list/SUM_FOLDL_', ax, (![l : ('type/list/list' 'type/num/num')]: (('const/list/SUM' l) = (('const/list/FOLDL' 'type/num/num' 'type/num/num') 'const/arithmetic/+' 'const/num/0' l)))).
tt('thm/rich_list/IS_PREFIX_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/isPREFIX' A) ('const/list/NIL' A) l) = $true))).
tt('thm/rich_list/IS_PREFIX_1', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/isPREFIX' A) (('const/list/CONS' A) x l) ('const/list/NIL' A)) = $false))).
tt('thm/rich_list/IS_PREFIX_e2', ax, ![A : $t]: (![x1 : A, l1 : ('type/list/list' A), x2 : A, l2 : ('type/list/list' A)]: ((('const/list/isPREFIX' A) (('const/list/CONS' A) x2 l2) (('const/list/CONS' A) x1 l1)) = ((x1 = x2) & (('const/list/isPREFIX' A) l2 l1))))).
tt('thm/rich_list/IS_PREFIX_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/isPREFIX' A) l2 l1) = (?[l : ('type/list/list' A)]: (l1 = (('const/list/APPEND' A) l2 l)))))).
tt('thm/rich_list/IS_SUFFIX_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) l1 l2) = (?[l : ('type/list/list' A)]: (l1 = (('const/list/APPEND' A) l l2)))))).
tt('thm/rich_list/IS_SUBLIST_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUBLIST' A) l1 l2) = (?[l : ('type/list/list' A), 'l\'' : ('type/list/list' A)]: (l1 = (('const/list/APPEND' A) l (('const/list/APPEND' A) l2 'l\''))))))).
tt('thm/rich_list/IS_PREFIX_IS_SUBLIST_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/isPREFIX' A) l2 l1) => (('const/rich_list/IS_SUBLIST' A) l1 l2)))).
tt('thm/rich_list/IS_SUFFIX_IS_SUBLIST_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) l1 l2) => (('const/rich_list/IS_SUBLIST' A) l1 l2)))).
tt('thm/rich_list/IS_PREFIX_REVERSE_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/isPREFIX' A) (('const/list/REVERSE' A) l2) (('const/list/REVERSE' A) l1)) = (('const/rich_list/IS_SUFFIX' A) l1 l2)))).
tt('thm/rich_list/IS_SUFFIX_REVERSE_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) (('const/list/REVERSE' A) l1) (('const/list/REVERSE' A) l2)) = (('const/list/isPREFIX' A) l2 l1)))).
tt('thm/rich_list/IS_SUFFIX_CONS2_E_', ax, ![A : $t]: (![s : ('type/list/list' A), h : A, t : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) s (('const/list/CONS' A) h t)) => (('const/rich_list/IS_SUFFIX' A) s t)))).
tt('thm/rich_list/IS_SUFFIX_REFL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (('const/rich_list/IS_SUFFIX' A) l l))).
tt('thm/rich_list/IS_SUBLIST_REVERSE_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUBLIST' A) (('const/list/REVERSE' A) l1) (('const/list/REVERSE' A) l2)) = (('const/rich_list/IS_SUBLIST' A) l1 l2)))).
tt('thm/rich_list/PREFIX_FOLDR_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/rich_list/PREFIX' A) P l) = (('const/list/FOLDR' A ('type/list/list' A)) (^[x : A, 'l\'' : ('type/list/list' A)]: (('const/bool/COND' ('type/list/list' A)) (P x) (('const/list/CONS' A) x 'l\'') ('const/list/NIL' A))) ('const/list/NIL' A) l)))).
tt('thm/rich_list/PREFIX_0', ax, ![A : $t]: (![P : (A > $o)]: ((('const/rich_list/PREFIX' A) P ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/rich_list/PREFIX_e1', ax, ![B : $t]: (![P : (B > $o), x : B, l : ('type/list/list' B)]: ((('const/rich_list/PREFIX' B) P (('const/list/CONS' B) x l)) = (('const/bool/COND' ('type/list/list' B)) (P x) (('const/list/CONS' B) x (('const/rich_list/PREFIX' B) P l)) ('const/list/NIL' B))))).
tt('thm/rich_list/IS_PREFIX_PREFIX_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: (('const/list/isPREFIX' A) (('const/rich_list/PREFIX' A) P l) l))).
tt('thm/rich_list/LENGTH_SCANL_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), e : A, l : ('type/list/list' B)]: ((('const/list/LENGTH' A) (('const/rich_list/SCANL' B A) f e l)) = ('const/num/SUC' (('const/list/LENGTH' B) l))))).
tt('thm/rich_list/LENGTH_SCANR_', ax, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, l : ('type/list/list' A)]: ((('const/list/LENGTH' B) (('const/rich_list/SCANR' A B) f e l)) = ('const/num/SUC' (('const/list/LENGTH' A) l))))).
tt('thm/rich_list/COMM_MONOID_FOLDL_', ax, ![A : $t]: (![f : (A > (A > A))]: ((('const/operator/COMM' A A) f) => (!['e\'' : A]: ((('const/operator/MONOID' A) f 'e\'') => (![e : A, l : ('type/list/list' A)]: ((('const/list/FOLDL' A A) f e l) = (f e (('const/list/FOLDL' A A) f 'e\'' l))))))))).
tt('thm/rich_list/COMM_MONOID_FOLDR_', ax, ![A : $t]: (![f : (A > (A > A))]: ((('const/operator/COMM' A A) f) => (!['e\'' : A]: ((('const/operator/MONOID' A) f 'e\'') => (![e : A, l : ('type/list/list' A)]: ((('const/list/FOLDR' A A) f e l) = (f e (('const/list/FOLDR' A A) f 'e\'' l))))))))).
tt('thm/rich_list/FCOMM_FOLDR_APPEND_', ax, ![B : $t, A : $t]: (![g : (A > (A > A)), f : (B > (A > A))]: ((('const/operator/FCOMM' A A B) g f) => (![e : A]: ((('const/operator/LEFT_ID' A A) g e) => (![l1 : ('type/list/list' B), l2 : ('type/list/list' B)]: ((('const/list/FOLDR' B A) f e (('const/list/APPEND' B) l1 l2)) = (g (('const/list/FOLDR' B A) f e l1) (('const/list/FOLDR' B A) f e l2))))))))).
tt('thm/rich_list/FCOMM_FOLDL_APPEND_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), g : (A > (A > A))]: ((('const/operator/FCOMM' A B A) f g) => (![e : A]: ((('const/operator/RIGHT_ID' A A) g e) => (![l1 : ('type/list/list' B), l2 : ('type/list/list' B)]: ((('const/list/FOLDL' B A) f e (('const/list/APPEND' B) l1 l2)) = (g (('const/list/FOLDL' B A) f e l1) (('const/list/FOLDL' B A) f e l2))))))))).
tt('thm/rich_list/FOLDL_SINGLE_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), e : A, x : B]: ((('const/list/FOLDL' B A) f e (('const/list/CONS' B) x ('const/list/NIL' B))) = (f e x)))).
tt('thm/rich_list/FOLDR_SINGLE_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), e : B, x : A]: ((('const/list/FOLDR' A B) f e (('const/list/CONS' A) x ('const/list/NIL' A))) = (f x e)))).
tt('thm/rich_list/FOLDR_CONS_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/FOLDR' A ('type/list/list' A)) ('const/list/CONS' A) ('const/list/NIL' A) l) = l))).
tt('thm/rich_list/FOLDL_SNOC_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/FOLDL' A ('type/list/list' A)) (^[xs : ('type/list/list' A), x : A]: (('const/list/SNOC' A) x xs)) ('const/list/NIL' A) l) = l))).
tt('thm/rich_list/FOLDR_FOLDL_REVERSE_', ax, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, l : ('type/list/list' A)]: ((('const/list/FOLDR' A B) f e l) = (('const/list/FOLDL' A B) (^[x : B, y : A]: (f y x)) e (('const/list/REVERSE' A) l))))).
tt('thm/rich_list/FOLDL_FOLDR_REVERSE_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), e : A, l : ('type/list/list' B)]: ((('const/list/FOLDL' B A) f e l) = (('const/list/FOLDR' B A) (^[x : B, y : A]: (f y x)) e (('const/list/REVERSE' B) l))))).
tt('thm/rich_list/FOLDR_REVERSE_', ax, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, l : ('type/list/list' A)]: ((('const/list/FOLDR' A B) f e (('const/list/REVERSE' A) l)) = (('const/list/FOLDL' A B) (^[x : B, y : A]: (f y x)) e l)))).
tt('thm/rich_list/FOLDL_REVERSE_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), e : A, l : ('type/list/list' B)]: ((('const/list/FOLDL' B A) f e (('const/list/REVERSE' B) l)) = (('const/list/FOLDR' B A) (^[x : B, y : A]: (f y x)) e l)))).
tt('thm/rich_list/FOLDR_MAP_', ax, ![C : $t, B : $t, A : $t]: (![f : (A > (B > B)), e : B, g : (C > A), l : ('type/list/list' C)]: ((('const/list/FOLDR' A B) f e (('const/list/MAP' C A) g l)) = (('const/list/FOLDR' C B) (^[x : C, y : B]: (f (g x) y)) e l)))).
tt('thm/rich_list/FOLDL_MAP_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > (B > A)), e : A, g : (C > B), l : ('type/list/list' C)]: ((('const/list/FOLDL' B A) f e (('const/list/MAP' C B) g l)) = (('const/list/FOLDL' C A) (^[x : A, y : C]: (f x (g y))) e l)))).
tt('thm/rich_list/EVERY_FOLDR_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) = (('const/list/FOLDR' A $o) (^[x : A, 'l\'' : $o]: ((P x) & 'l\'')) $true l)))).
tt('thm/rich_list/EVERY_FOLDL_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) = (('const/list/FOLDL' A $o) (^['l\'' : $o, x : A]: ('l\'' & (P x))) $true l)))).
tt('thm/rich_list/EXISTS_FOLDR_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P l) = (('const/list/FOLDR' A $o) (^[x : A, 'l\'' : $o]: ((P x) | 'l\'')) $false l)))).
tt('thm/rich_list/EXISTS_FOLDL_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P l) = (('const/list/FOLDL' A $o) (^['l\'' : $o, x : A]: ('l\'' | (P x))) $false l)))).
tt('thm/rich_list/EVERY_FOLDR_MAP_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) = (('const/list/FOLDR' $o $o) $and $true (('const/list/MAP' A $o) P l))))).
tt('thm/rich_list/EVERY_FOLDL_MAP_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) = (('const/list/FOLDL' $o $o) $and $true (('const/list/MAP' A $o) P l))))).
tt('thm/rich_list/EXISTS_FOLDR_MAP_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P l) = (('const/list/FOLDR' $o $o) $or $false (('const/list/MAP' A $o) P l))))).
tt('thm/rich_list/EXISTS_FOLDL_MAP_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P l) = (('const/list/FOLDL' $o $o) $or $false (('const/list/MAP' A $o) P l))))).
tt('thm/rich_list/FOLDR_FILTER_', ax, ![A : $t, B : $t]: (![f : (A > (B > B)), e : B, P : (A > $o), l : ('type/list/list' A)]: ((('const/list/FOLDR' A B) f e (('const/list/FILTER' A) P l)) = (('const/list/FOLDR' A B) (^[x : A, y : B]: (('const/bool/COND' B) (P x) (f x y) y)) e l)))).
tt('thm/rich_list/FOLDL_FILTER_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), e : A, P : (B > $o), l : ('type/list/list' B)]: ((('const/list/FOLDL' B A) f e (('const/list/FILTER' B) P l)) = (('const/list/FOLDL' B A) (^[x : A, y : B]: (('const/bool/COND' A) (P y) (f x y) x)) e l)))).
tt('thm/rich_list/ASSOC_FOLDR_FLAT_', ax, ![A : $t]: (![f : (A > (A > A))]: ((('const/operator/ASSOC' A) f) => (![e : A]: ((('const/operator/LEFT_ID' A A) f e) => (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FOLDR' A A) f e (('const/list/FLAT' A) l)) = (('const/list/FOLDR' A A) f e (('const/list/MAP' ('type/list/list' A) A) (('const/list/FOLDR' A A) f e) l))))))))).
tt('thm/rich_list/ASSOC_FOLDL_FLAT_', ax, ![A : $t]: (![f : (A > (A > A))]: ((('const/operator/ASSOC' A) f) => (![e : A]: ((('const/operator/RIGHT_ID' A A) f e) => (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FOLDL' A A) f e (('const/list/FLAT' A) l)) = (('const/list/FOLDL' A A) f e (('const/list/MAP' ('type/list/list' A) A) (('const/list/FOLDL' A A) f e) l))))))))).
tt('thm/rich_list/MAP_FLAT_', ax, ![A : $t, B : $t]: (![f : (A > B), l : ('type/list/list' ('type/list/list' A))]: ((('const/list/MAP' A B) f (('const/list/FLAT' A) l)) = (('const/list/FLAT' B) (('const/list/MAP' ('type/list/list' A) ('type/list/list' B)) (('const/list/MAP' A B) f) l))))).
tt('thm/rich_list/FILTER_FLAT_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FILTER' A) P (('const/list/FLAT' A) l)) = (('const/list/FLAT' A) (('const/list/MAP' ('type/list/list' A) ('type/list/list' A)) (('const/list/FILTER' A) P) l))))).
tt('thm/rich_list/EXISTS_DISJ_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) (^[x : A]: ((P x) | (Q x))) l) = ((('const/list/EXISTS' A) P l) | (('const/list/EXISTS' A) Q l))))).
tt('thm/rich_list/MEM_FOLDR_', ax, ![A : $t]: (![y : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) l)) = (('const/list/FOLDR' A $o) (^[x : A, 'l\'' : $o]: ((y = x) | 'l\'')) $false l)))).
tt('thm/rich_list/MEM_FOLDL_', ax, ![A : $t]: (![y : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) l)) = (('const/list/FOLDL' A $o) (^['l\'' : $o, x : A]: ('l\'' | (y = x))) $false l)))).
tt('thm/rich_list/NULL_FOLDR_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/NULL' A) l) = (('const/list/FOLDR' A $o) (^[x : A, 'l\'' : $o]: $false) $true l)))).
tt('thm/rich_list/NULL_FOLDL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/NULL' A) l) = (('const/list/FOLDL' A $o) (^[x : $o, 'l\'' : A]: $false) $true l)))).
tt('thm/rich_list/MAP_REVERSE_', ax, ![A : $t, B : $t]: (![f : (A > B), l : ('type/list/list' A)]: ((('const/list/MAP' A B) f (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' B) (('const/list/MAP' A B) f l))))).
tt('thm/rich_list/SEG_LENGTH_ID_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) (('const/list/LENGTH' A) l) 'const/num/0' l) = l))).
tt('thm/rich_list/SEG_SUC_CONS_', ax, ![A : $t]: (![m : 'type/num/num', n : 'type/num/num', l : ('type/list/list' A), x : A]: ((('const/rich_list/SEG' A) m ('const/num/SUC' n) (('const/list/CONS' A) x l)) = (('const/rich_list/SEG' A) m n l)))).
tt('thm/rich_list/SEG_0_SNOC_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A), x : A]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => ((('const/rich_list/SEG' A) m 'const/num/0' (('const/list/SNOC' A) x l)) = (('const/rich_list/SEG' A) m 'const/num/0' l))))).
tt('thm/rich_list/BUTLASTN_SEG_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) n l) = (('const/rich_list/SEG' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) 'const/num/0' l))))).
tt('thm/rich_list/LASTN_CONS_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/rich_list/LASTN' A) n (('const/list/CONS' A) x l)) = (('const/rich_list/LASTN' A) n l)))))).
tt('thm/rich_list/LENGTH_LASTN_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/LENGTH' A) (('const/rich_list/LASTN' A) n l)) = n)))).
tt('thm/rich_list/LASTN_LENGTH_ID_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) (('const/list/LENGTH' A) l) l) = l))).
tt('thm/rich_list/LASTN_LASTN_', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (('const/arithmetic/<=' n m) => ((('const/rich_list/LASTN' A) n (('const/rich_list/LASTN' A) m l)) = (('const/rich_list/LASTN' A) n l)))))).
tt('thm/rich_list/TAKE_SNOC_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/list/TAKE' A) n (('const/list/SNOC' A) x l)) = (('const/list/TAKE' A) n l)))))).
tt('thm/rich_list/BUTLASTN_SUC_FRONT_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) ('const/num/SUC' n) l) = (('const/rich_list/BUTLASTN' A) n (('const/list/FRONT' A) l)))))).
tt('thm/rich_list/BUTLASTN_FRONT_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) n (('const/list/FRONT' A) l)) = (('const/list/FRONT' A) (('const/rich_list/BUTLASTN' A) n l)))))).
tt('thm/rich_list/LENGTH_BUTLASTN_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/LENGTH' A) (('const/rich_list/BUTLASTN' A) n l)) = ('const/arithmetic/-' (('const/list/LENGTH' A) l) n))))).
tt('thm/rich_list/BUTLASTN_BUTLASTN_', ax, ![A : $t]: (![m : 'type/num/num', n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) n (('const/rich_list/BUTLASTN' A) m l)) = (('const/rich_list/BUTLASTN' A) ('const/arithmetic/+' n m) l))))).
tt('thm/rich_list/APPEND_BUTLASTN_LASTN_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/APPEND' A) (('const/rich_list/BUTLASTN' A) n l) (('const/rich_list/LASTN' A) n l)) = l)))).
tt('thm/rich_list/APPEND_TAKE_LASTN_', ax, ![A : $t]: (![m : 'type/num/num', n : 'type/num/num', l : ('type/list/list' A)]: ((('const/arithmetic/+' m n) = (('const/list/LENGTH' A) l)) => ((('const/list/APPEND' A) (('const/list/TAKE' A) n l) (('const/rich_list/LASTN' A) m l)) = l)))).
tt('thm/rich_list/BUTLASTN_APPEND2_', ax, ![A : $t]: (![n : 'type/num/num', l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l2)) => ((('const/rich_list/BUTLASTN' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) l1 (('const/rich_list/BUTLASTN' A) n l2)))))).
tt('thm/rich_list/BUTLASTN_LENGTH_APPEND_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A)]: ((('const/rich_list/BUTLASTN' A) (('const/list/LENGTH' A) l2) (('const/list/APPEND' A) l1 l2)) = l1))).
tt('thm/rich_list/LASTN_LENGTH_APPEND_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) (('const/list/LENGTH' A) l2) (('const/list/APPEND' A) l1 l2)) = l2))).
tt('thm/rich_list/BUTLASTN_CONS_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/rich_list/BUTLASTN' A) n (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/rich_list/BUTLASTN' A) n l))))))).
tt('thm/rich_list/BUTLASTN_LENGTH_CONS_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/rich_list/BUTLASTN' A) (('const/list/LENGTH' A) l) (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x ('const/list/NIL' A))))).
tt('thm/rich_list/LAST_LASTN_LAST_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (('const/prim_rec/<' 'const/num/0' n) => ((('const/list/LAST' A) (('const/rich_list/LASTN' A) n l)) = (('const/list/LAST' A) l)))))).
tt('thm/rich_list/BUTLASTN_LASTN_NIL_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) n (('const/rich_list/LASTN' A) n l)) = ('const/list/NIL' A))))).
tt('thm/rich_list/LASTN_BUTLASTN_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => ((('const/rich_list/LASTN' A) n (('const/rich_list/BUTLASTN' A) m l)) = (('const/rich_list/BUTLASTN' A) m (('const/rich_list/LASTN' A) ('const/arithmetic/+' n m) l)))))).
tt('thm/rich_list/BUTLASTN_LASTN_', ax, ![A : $t]: (![m : 'type/num/num', n : 'type/num/num', l : ('type/list/list' A)]: ((('const/arithmetic/<=' m n) & ('const/arithmetic/<=' n (('const/list/LENGTH' A) l))) => ((('const/rich_list/BUTLASTN' A) m (('const/rich_list/LASTN' A) n l)) = (('const/rich_list/LASTN' A) ('const/arithmetic/-' n m) (('const/rich_list/BUTLASTN' A) m l)))))).
tt('thm/rich_list/LASTN_1_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (l = ('const/list/NIL' A))) => ((('const/rich_list/LASTN' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) l) = (('const/list/CONS' A) (('const/list/LAST' A) l) ('const/list/NIL' A)))))).
tt('thm/rich_list/BUTLASTN_1_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (l = ('const/list/NIL' A))) => ((('const/rich_list/BUTLASTN' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) l) = (('const/list/FRONT' A) l))))).
tt('thm/rich_list/BUTLASTN_APPEND1_', ax, ![A : $t]: (![l2 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l2) n) => (![l1 : ('type/list/list' A)]: ((('const/rich_list/BUTLASTN' A) n (('const/list/APPEND' A) l1 l2)) = (('const/rich_list/BUTLASTN' A) ('const/arithmetic/-' n (('const/list/LENGTH' A) l2)) l1)))))).
tt('thm/rich_list/LASTN_APPEND2_', ax, ![A : $t]: (![n : 'type/num/num', l2 : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l2)) => (![l1 : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) n (('const/list/APPEND' A) l1 l2)) = (('const/rich_list/LASTN' A) n l2)))))).
tt('thm/rich_list/LASTN_APPEND1_', ax, ![A : $t]: (![l2 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l2) n) => (![l1 : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/rich_list/LASTN' A) ('const/arithmetic/-' n (('const/list/LENGTH' A) l2)) l1) l2)))))).
tt('thm/rich_list/LASTN_MAP_', ax, ![A : $t, B : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (![f : (A > B)]: ((('const/rich_list/LASTN' B) n (('const/list/MAP' A B) f l)) = (('const/list/MAP' A B) f (('const/rich_list/LASTN' A) n l))))))).
tt('thm/rich_list/BUTLASTN_MAP_', ax, ![A : $t, B : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (![f : (A > B)]: ((('const/rich_list/BUTLASTN' B) n (('const/list/MAP' A B) f l)) = (('const/list/MAP' A B) f (('const/rich_list/BUTLASTN' A) n l))))))).
tt('thm/rich_list/EVERY_LASTN_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) => (![m : 'type/num/num']: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (('const/list/EVERY' A) P (('const/rich_list/LASTN' A) m l))))))).
tt('thm/rich_list/EVERY_BUTLASTN_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) => (![m : 'type/num/num']: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (('const/list/EVERY' A) P (('const/rich_list/BUTLASTN' A) m l))))))).
tt('thm/rich_list/TAKE_TAKE_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![n : 'type/num/num']: (('const/arithmetic/<=' n m) => ((('const/list/TAKE' A) n (('const/list/TAKE' A) m l)) = (('const/list/TAKE' A) n l))))))).
tt('thm/rich_list/DROP_LENGTH_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/DROP' A) (('const/list/LENGTH' A) l) l) = ('const/list/NIL' A)))).
tt('thm/rich_list/BUTLASTN_LENGTH_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/rich_list/BUTLASTN' A) (('const/list/LENGTH' A) l) l) = ('const/list/NIL' A)))).
tt('thm/rich_list/DROP_APPEND1_', ax, ![A : $t]: (![n : 'type/num/num', l1 : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l1)) => (![l2 : ('type/list/list' A)]: ((('const/list/DROP' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/list/DROP' A) n l1) l2)))))).
tt('thm/rich_list/DROP_APPEND2_', ax, ![A : $t]: (![l1 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l1) n) => (![l2 : ('type/list/list' A)]: ((('const/list/DROP' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/DROP' A) ('const/arithmetic/-' n (('const/list/LENGTH' A) l1)) l2)))))).
tt('thm/rich_list/DROP_DROP_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => ((('const/list/DROP' A) n (('const/list/DROP' A) m l)) = (('const/list/DROP' A) ('const/arithmetic/+' n m) l))))).
tt('thm/rich_list/LASTN_SEG_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/LASTN' A) n l) = (('const/rich_list/SEG' A) n ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) l))))).
tt('thm/rich_list/TAKE_SEG_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/TAKE' A) n l) = (('const/rich_list/SEG' A) n 'const/num/0' l))))).
tt('thm/rich_list/DROP_SEG_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/DROP' A) n l) = (('const/rich_list/SEG' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) n l))))).
tt('thm/rich_list/DROP_SNOC_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/list/DROP' A) n (('const/list/SNOC' A) x l)) = (('const/list/SNOC' A) x (('const/list/DROP' A) n l))))))).
tt('thm/rich_list/APPEND_BUTLASTN_DROP_', ax, ![A : $t]: (![m : 'type/num/num', n : 'type/num/num', l : ('type/list/list' A)]: ((('const/arithmetic/+' m n) = (('const/list/LENGTH' A) l)) => ((('const/list/APPEND' A) (('const/rich_list/BUTLASTN' A) m l) (('const/list/DROP' A) n l)) = l)))).
tt('thm/rich_list/SEG_SEG_', ax, ![A : $t]: (![n1 : 'type/num/num', m1 : 'type/num/num', n2 : 'type/num/num', m2 : 'type/num/num', l : ('type/list/list' A)]: ((('const/arithmetic/<=' ('const/arithmetic/+' n1 m1) (('const/list/LENGTH' A) l)) & ('const/arithmetic/<=' ('const/arithmetic/+' n2 m2) n1)) => ((('const/rich_list/SEG' A) n2 m2 (('const/rich_list/SEG' A) n1 m1 l)) = (('const/rich_list/SEG' A) n2 ('const/arithmetic/+' m1 m2) l))))).
tt('thm/rich_list/SEG_APPEND1_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l1 : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l1)) => (![l2 : ('type/list/list' A)]: ((('const/rich_list/SEG' A) n m (('const/list/APPEND' A) l1 l2)) = (('const/rich_list/SEG' A) n m l1)))))).
tt('thm/rich_list/SEG_APPEND2_', ax, ![A : $t]: (![l1 : ('type/list/list' A), m : 'type/num/num', n : 'type/num/num', l2 : ('type/list/list' A)]: ((('const/arithmetic/<=' (('const/list/LENGTH' A) l1) m) & ('const/arithmetic/<=' n (('const/list/LENGTH' A) l2))) => ((('const/rich_list/SEG' A) n m (('const/list/APPEND' A) l1 l2)) = (('const/rich_list/SEG' A) n ('const/arithmetic/-' m (('const/list/LENGTH' A) l1)) l2))))).
tt('thm/rich_list/SEG_TAKE_BUTFISTN_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => ((('const/rich_list/SEG' A) n m l) = (('const/list/TAKE' A) n (('const/list/DROP' A) m l)))))).
tt('thm/rich_list/SEG_APPEND_', ax, ![A : $t]: (![m : 'type/num/num', l1 : ('type/list/list' A), n : 'type/num/num', l2 : ('type/list/list' A)]: ((('const/prim_rec/<' m (('const/list/LENGTH' A) l1)) & (('const/arithmetic/<=' (('const/list/LENGTH' A) l1) ('const/arithmetic/+' n m)) & ('const/arithmetic/<=' ('const/arithmetic/+' n m) ('const/arithmetic/+' (('const/list/LENGTH' A) l1) (('const/list/LENGTH' A) l2))))) => ((('const/rich_list/SEG' A) n m (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/rich_list/SEG' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l1) m) m l1) (('const/rich_list/SEG' A) ('const/arithmetic/-' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l1)) 'const/num/0' l2)))))).
tt('thm/rich_list/SEG_LENGTH_SNOC_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/list/LENGTH' A) l) (('const/list/SNOC' A) x l)) = (('const/list/CONS' A) x ('const/list/NIL' A))))).
tt('thm/rich_list/SEG_SNOC_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/rich_list/SEG' A) n m (('const/list/SNOC' A) x l)) = (('const/rich_list/SEG' A) n m l)))))).
tt('thm/rich_list/ELL_SEG_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/ELL' A) n l) = (('const/list/HD' A) (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/prim_rec/PRE' ('const/arithmetic/-' (('const/list/LENGTH' A) l) n)) l)))))).
tt('thm/rich_list/SNOC_FOLDR_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/SNOC' A) x l) = (('const/list/FOLDR' A ('type/list/list' A)) ('const/list/CONS' A) (('const/list/CONS' A) x ('const/list/NIL' A)) l)))).
tt('thm/rich_list/MEM_FOLDR_MAP_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) = (('const/list/FOLDR' $o $o) $or $false (('const/list/MAP' A $o) (($equals A) x) l))))).
tt('thm/rich_list/MEM_FOLDL_MAP_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) = (('const/list/FOLDL' $o $o) $or $false (('const/list/MAP' A $o) (($equals A) x) l))))).
tt('thm/rich_list/FILTER_FILTER_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o), l : ('type/list/list' A)]: ((('const/list/FILTER' A) P (('const/list/FILTER' A) Q l)) = (('const/list/FILTER' A) (^[x : A]: ((P x) & (Q x))) l)))).
tt('thm/rich_list/FCOMM_FOLDR_FLAT_', ax, ![B : $t, A : $t]: (![g : (A > (A > A)), f : (B > (A > A))]: ((('const/operator/FCOMM' A A B) g f) => (![e : A]: ((('const/operator/LEFT_ID' A A) g e) => (![l : ('type/list/list' ('type/list/list' B))]: ((('const/list/FOLDR' B A) f e (('const/list/FLAT' B) l)) = (('const/list/FOLDR' A A) g e (('const/list/MAP' ('type/list/list' B) A) (('const/list/FOLDR' B A) f e) l))))))))).
tt('thm/rich_list/FCOMM_FOLDL_FLAT_', ax, ![B : $t, A : $t]: (![f : (A > (B > A)), g : (A > (A > A))]: ((('const/operator/FCOMM' A B A) f g) => (![e : A]: ((('const/operator/RIGHT_ID' A A) g e) => (![l : ('type/list/list' ('type/list/list' B))]: ((('const/list/FOLDL' B A) f e (('const/list/FLAT' B) l)) = (('const/list/FOLDL' A A) g e (('const/list/MAP' ('type/list/list' B) A) (('const/list/FOLDL' B A) f e) l))))))))).
tt('thm/rich_list/FOLDR_MAP_REVERSE_', ax, ![B : $t, A : $t]: (![f : (A > (A > A))]: ((![a : A, b : A, c : A]: ((f a (f b c)) = (f b (f a c)))) => (![e : A, g : (B > A), l : ('type/list/list' B)]: ((('const/list/FOLDR' A A) f e (('const/list/MAP' B A) g (('const/list/REVERSE' B) l))) = (('const/list/FOLDR' A A) f e (('const/list/MAP' B A) g l))))))).
tt('thm/rich_list/FOLDR_FILTER_REVERSE_', ax, ![A : $t]: (![f : (A > (A > A))]: ((![a : A, b : A, c : A]: ((f a (f b c)) = (f b (f a c)))) => (![e : A, P : (A > $o), l : ('type/list/list' A)]: ((('const/list/FOLDR' A A) f e (('const/list/FILTER' A) P (('const/list/REVERSE' A) l))) = (('const/list/FOLDR' A A) f e (('const/list/FILTER' A) P l))))))).
tt('thm/rich_list/COMM_ASSOC_FOLDR_REVERSE_', ax, ![A : $t]: (![f : (A > (A > A))]: ((('const/operator/COMM' A A) f) => ((('const/operator/ASSOC' A) f) => (![e : A, l : ('type/list/list' A)]: ((('const/list/FOLDR' A A) f e (('const/list/REVERSE' A) l)) = (('const/list/FOLDR' A A) f e l))))))).
tt('thm/rich_list/COMM_ASSOC_FOLDL_REVERSE_', ax, ![A : $t]: (![f : (A > (A > A))]: ((('const/operator/COMM' A A) f) => ((('const/operator/ASSOC' A) f) => (![e : A, l : ('type/list/list' A)]: ((('const/list/FOLDL' A A) f e (('const/list/REVERSE' A) l)) = (('const/list/FOLDL' A A) f e l))))))).
tt('thm/rich_list/ELL_LAST_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (('const/list/NULL' A) l)) => ((('const/rich_list/ELL' A) 'const/num/0' l) = (('const/list/LAST' A) l))))).
tt('thm/rich_list/ELL_0_SNOC_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/rich_list/ELL' A) 'const/num/0' (('const/list/SNOC' A) x l)) = x))).
tt('thm/rich_list/ELL_SNOC_', ax, ![A : $t]: (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![x : A, l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) n (('const/list/SNOC' A) x l)) = (('const/rich_list/ELL' A) ('const/prim_rec/PRE' n) l)))))).
tt('thm/rich_list/ELL_SUC_SNOC_', ax, ![A : $t]: (![n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/ELL' A) ('const/num/SUC' n) (('const/list/SNOC' A) x l)) = (('const/rich_list/ELL' A) n l)))).
tt('thm/rich_list/ELL_CONS_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/rich_list/ELL' A) n (('const/list/CONS' A) x l)) = (('const/rich_list/ELL' A) n l)))))).
tt('thm/rich_list/ELL_LENGTH_CONS_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/rich_list/ELL' A) (('const/list/LENGTH' A) l) (('const/list/CONS' A) x l)) = x))).
tt('thm/rich_list/ELL_LENGTH_SNOC_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/rich_list/ELL' A) (('const/list/LENGTH' A) l) (('const/list/SNOC' A) x l)) = (('const/bool/COND' A) (('const/list/NULL' A) l) x (('const/list/HD' A) l))))).
tt('thm/rich_list/ELL_APPEND2_', ax, ![A : $t]: (![n : 'type/num/num', l2 : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l2)) => (![l1 : ('type/list/list' A)]: ((('const/rich_list/ELL' A) n (('const/list/APPEND' A) l1 l2)) = (('const/rich_list/ELL' A) n l2)))))).
tt('thm/rich_list/ELL_APPEND1_', ax, ![A : $t]: (![l2 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l2) n) => (![l1 : ('type/list/list' A)]: ((('const/rich_list/ELL' A) n (('const/list/APPEND' A) l1 l2)) = (('const/rich_list/ELL' A) ('const/arithmetic/-' n (('const/list/LENGTH' A) l2)) l1)))))).
tt('thm/rich_list/ELL_PRE_LENGTH_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (l = ('const/list/NIL' A))) => ((('const/rich_list/ELL' A) ('const/prim_rec/PRE' (('const/list/LENGTH' A) l)) l) = (('const/list/HD' A) l))))).
tt('thm/rich_list/EL_PRE_LENGTH_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (l = ('const/list/NIL' A))) => ((('const/list/EL' A) ('const/prim_rec/PRE' (('const/list/LENGTH' A) l)) l) = (('const/list/LAST' A) l))))).
tt('thm/rich_list/EL_ELL_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/list/EL' A) n l) = (('const/rich_list/ELL' A) ('const/prim_rec/PRE' ('const/arithmetic/-' (('const/list/LENGTH' A) l) n)) l))))).
tt('thm/rich_list/EL_LENGTH_APPEND_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A)]: ((~ (('const/list/NULL' A) l2)) => ((('const/list/EL' A) (('const/list/LENGTH' A) l1) (('const/list/APPEND' A) l1 l2)) = (('const/list/HD' A) l2))))).
tt('thm/rich_list/ELL_EL_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/ELL' A) n l) = (('const/list/EL' A) ('const/prim_rec/PRE' ('const/arithmetic/-' (('const/list/LENGTH' A) l) n)) l))))).
tt('thm/rich_list/ELL_MAP_', ax, ![A : $t, B : $t]: (![n : 'type/num/num', l : ('type/list/list' A), f : (A > B)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/ELL' B) n (('const/list/MAP' A B) f l)) = (f (('const/rich_list/ELL' A) n l)))))).
tt('thm/rich_list/LENGTH_FRONT_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (l = ('const/list/NIL' A))) => ((('const/list/LENGTH' A) (('const/list/FRONT' A) l)) = ('const/prim_rec/PRE' (('const/list/LENGTH' A) l)))))).
tt('thm/rich_list/DROP_LENGTH_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/DROP' A) (('const/list/LENGTH' A) l1) (('const/list/APPEND' A) l1 l2)) = l2))).
tt('thm/rich_list/TAKE_APPEND1_', ax, ![A : $t]: (![n : 'type/num/num', l1 : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l1)) => (![l2 : ('type/list/list' A)]: ((('const/list/TAKE' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/TAKE' A) n l1)))))).
tt('thm/rich_list/TAKE_APPEND2_', ax, ![A : $t]: (![l1 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l1) n) => (![l2 : ('type/list/list' A)]: ((('const/list/TAKE' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) l1 (('const/list/TAKE' A) ('const/arithmetic/-' n (('const/list/LENGTH' A) l1)) l2))))))).
tt('thm/rich_list/TAKE_LENGTH_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/TAKE' A) (('const/list/LENGTH' A) l1) (('const/list/APPEND' A) l1 l2)) = l1))).
tt('thm/rich_list/REVERSE_FLAT_', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/REVERSE' A) (('const/list/FLAT' A) l)) = (('const/list/FLAT' A) (('const/list/REVERSE' ('type/list/list' A)) (('const/list/MAP' ('type/list/list' A) ('type/list/list' A)) ('const/list/REVERSE' A) l)))))).
tt('thm/rich_list/MAP_FILTER_', ax, ![A : $t]: (![f : (A > A), P : (A > $o), l : ('type/list/list' A)]: ((![x : A]: ((P (f x)) = (P x))) => ((('const/list/MAP' A A) f (('const/list/FILTER' A) P l)) = (('const/list/FILTER' A) P (('const/list/MAP' A A) f l)))))).
tt('thm/rich_list/FLAT_REVERSE_', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/FLAT' A) (('const/list/REVERSE' ('type/list/list' A)) l)) = (('const/list/REVERSE' A) (('const/list/FLAT' A) (('const/list/MAP' ('type/list/list' A) ('type/list/list' A)) ('const/list/REVERSE' A) l)))))).
tt('thm/rich_list/FLAT_FLAT_', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' ('type/list/list' A)))]: ((('const/list/FLAT' A) (('const/list/FLAT' ('type/list/list' A)) l)) = (('const/list/FLAT' A) (('const/list/MAP' ('type/list/list' ('type/list/list' A)) ('type/list/list' A)) ('const/list/FLAT' A) l))))).
tt('thm/rich_list/EVERY_REVERSE_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P (('const/list/REVERSE' A) l)) = (('const/list/EVERY' A) P l)))).
tt('thm/rich_list/EXISTS_REVERSE_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P (('const/list/REVERSE' A) l)) = (('const/list/EXISTS' A) P l)))).
tt('thm/rich_list/EVERY_SEG_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) => (![m : 'type/num/num', k : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/+' m k) (('const/list/LENGTH' A) l)) => (('const/list/EVERY' A) P (('const/rich_list/SEG' A) m k l))))))).
tt('thm/rich_list/EVERY_TAKE_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) => (![m : 'type/num/num']: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (('const/list/EVERY' A) P (('const/list/TAKE' A) m l))))))).
tt('thm/rich_list/EVERY_DROP_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) => (![m : 'type/num/num']: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (('const/list/EVERY' A) P (('const/list/DROP' A) m l))))))).
tt('thm/rich_list/EXISTS_SEG_', ax, ![A : $t]: (![m : 'type/num/num', k : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' m k) (('const/list/LENGTH' A) l)) => (![P : (A > $o)]: ((('const/list/EXISTS' A) P (('const/rich_list/SEG' A) m k l)) => (('const/list/EXISTS' A) P l)))))).
tt('thm/rich_list/EXISTS_TAKE_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![P : (A > $o)]: ((('const/list/EXISTS' A) P (('const/list/TAKE' A) m l)) => (('const/list/EXISTS' A) P l)))))).
tt('thm/rich_list/EXISTS_DROP_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![P : (A > $o)]: ((('const/list/EXISTS' A) P (('const/list/DROP' A) m l)) => (('const/list/EXISTS' A) P l)))))).
tt('thm/rich_list/EXISTS_LASTN_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![P : (A > $o)]: ((('const/list/EXISTS' A) P (('const/rich_list/LASTN' A) m l)) => (('const/list/EXISTS' A) P l)))))).
tt('thm/rich_list/EXISTS_BUTLASTN_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![P : (A > $o)]: ((('const/list/EXISTS' A) P (('const/rich_list/BUTLASTN' A) m l)) => (('const/list/EXISTS' A) P l)))))).
tt('thm/rich_list/MEM_SEG_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/rich_list/SEG' A) n m l))) => (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/rich_list/MEM_TAKE_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/TAKE' A) m l))) => (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/rich_list/MEM_DROP_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/DROP' A) m l))) => (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/rich_list/MEM_BUTLASTN_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/rich_list/BUTLASTN' A) m l))) => (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/rich_list/MEM_LASTN_', ax, ![A : $t]: (![m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/rich_list/LASTN' A) m l))) => (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/rich_list/ZIP_SNOC_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => (![x1 : A, x2 : B]: ((('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/SNOC' A) x1 l1) (('const/list/SNOC' B) x2 l2))) = (('const/list/SNOC' ('type/pair/prod' A B)) (('const/pair/,' A B) x1 x2) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))))))).
tt('thm/rich_list/UNZIP_SNOC_', ax, ![A : $t, B : $t]: (![x : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/UNZIP' A B) (('const/list/SNOC' ('type/pair/prod' A B)) x l)) = (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/SNOC' A) (('const/pair/FST' A B) x) (('const/pair/FST' ('type/list/list' A) ('type/list/list' B)) (('const/list/UNZIP' A B) l))) (('const/list/SNOC' B) (('const/pair/SND' A B) x) (('const/pair/SND' ('type/list/list' A) ('type/list/list' B)) (('const/list/UNZIP' A B) l))))))).
tt('thm/rich_list/LENGTH_UNZIP_FST_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/LENGTH' A) (('const/rich_list/UNZIP_FST' A B) l)) = (('const/list/LENGTH' ('type/pair/prod' A B)) l)))).
tt('thm/rich_list/LENGTH_UNZIP_SND_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/LENGTH' B) (('const/rich_list/UNZIP_SND' B A) l)) = (('const/list/LENGTH' ('type/pair/prod' A B)) l)))).
tt('thm/rich_list/SUM_REVERSE_', ax, (![l : ('type/list/list' 'type/num/num')]: (('const/list/SUM' (('const/list/REVERSE' 'type/num/num') l)) = ('const/list/SUM' l)))).
tt('thm/rich_list/SUM_FLAT_', ax, (![l : ('type/list/list' ('type/list/list' 'type/num/num'))]: (('const/list/SUM' (('const/list/FLAT' 'type/num/num') l)) = ('const/list/SUM' (('const/list/MAP' ('type/list/list' 'type/num/num') 'type/num/num') 'const/list/SUM' l))))).
tt('thm/rich_list/EL_APPEND1_', ax, ![A : $t]: (![n : 'type/num/num', l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l1)) => ((('const/list/EL' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/EL' A) n l1))))).
tt('thm/rich_list/EL_APPEND2_', ax, ![A : $t]: (![l1 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l1) n) => (![l2 : ('type/list/list' A)]: ((('const/list/EL' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/EL' A) ('const/arithmetic/-' n (('const/list/LENGTH' A) l1)) l2)))))).
tt('thm/rich_list/LUPDATE_APPEND2_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), n : 'type/num/num', x : A]: (('const/arithmetic/<=' (('const/list/LENGTH' A) l1) n) => ((('const/list/LUPDATE' A) x n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) l1 (('const/list/LUPDATE' A) x ('const/arithmetic/-' n (('const/list/LENGTH' A) l1)) l2)))))).
tt('thm/rich_list/LUPDATE_APPEND1_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), n : 'type/num/num', x : A]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l1)) => ((('const/list/LUPDATE' A) x n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/list/LUPDATE' A) x n l1) l2))))).
tt('thm/rich_list/EL_CONS_', ax, ![A : $t]: (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![x : A, l : ('type/list/list' A)]: ((('const/list/EL' A) n (('const/list/CONS' A) x l)) = (('const/list/EL' A) ('const/prim_rec/PRE' n) l)))))).
tt('thm/rich_list/EL_SEG_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/list/EL' A) n l) = (('const/list/HD' A) (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n l)))))).
tt('thm/rich_list/EL_MEM_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (('const/bool/IN' A) (('const/list/EL' A) n l) (('const/list/LIST_TO_SET' A) l))))).
tt('thm/rich_list/TL_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/TL' A) (('const/list/SNOC' A) x l)) = (('const/bool/COND' ('type/list/list' A)) (('const/list/NULL' A) l) ('const/list/NIL' A) (('const/list/SNOC' A) x (('const/list/TL' A) l)))))).
tt('thm/rich_list/EL_REVERSE_ELL_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/list/EL' A) n (('const/list/REVERSE' A) l)) = (('const/rich_list/ELL' A) n l))))).
tt('thm/rich_list/ELL_LENGTH_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((~ (('const/list/NULL' A) l1)) => ((('const/rich_list/ELL' A) (('const/list/LENGTH' A) l2) (('const/list/APPEND' A) l1 l2)) = (('const/list/LAST' A) l1))))).
tt('thm/rich_list/ELL_MEM_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (('const/bool/IN' A) (('const/rich_list/ELL' A) n l) (('const/list/LIST_TO_SET' A) l))))).
tt('thm/rich_list/ELL_REVERSE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/ELL' A) n (('const/list/REVERSE' A) l)) = (('const/rich_list/ELL' A) ('const/prim_rec/PRE' ('const/arithmetic/-' (('const/list/LENGTH' A) l) n)) l))))).
tt('thm/rich_list/ELL_REVERSE_EL_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/ELL' A) n (('const/list/REVERSE' A) l)) = (('const/list/EL' A) n l))))).
tt('thm/rich_list/TAKE_BUTLASTN_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/TAKE' A) n l) = (('const/rich_list/BUTLASTN' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) l))))).
tt('thm/rich_list/BUTLASTN_TAKE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) n l) = (('const/list/TAKE' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) l))))).
tt('thm/rich_list/LASTN_DROP_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/LASTN' A) n l) = (('const/list/DROP' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) l))))).
tt('thm/rich_list/DROP_LASTN_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/DROP' A) n l) = (('const/rich_list/LASTN' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) n) l))))).
tt('thm/rich_list/SEG_LASTN_BUTLASTN_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => ((('const/rich_list/SEG' A) n m l) = (('const/rich_list/LASTN' A) n (('const/rich_list/BUTLASTN' A) ('const/arithmetic/-' (('const/list/LENGTH' A) l) ('const/arithmetic/+' n m)) l)))))).
tt('thm/rich_list/DROP_REVERSE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/DROP' A) n (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' A) (('const/rich_list/BUTLASTN' A) n l)))))).
tt('thm/rich_list/BUTLASTN_REVERSE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/BUTLASTN' A) n (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' A) (('const/list/DROP' A) n l)))))).
tt('thm/rich_list/LASTN_REVERSE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/rich_list/LASTN' A) n (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' A) (('const/list/TAKE' A) n l)))))).
tt('thm/rich_list/TAKE_REVERSE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l)) => ((('const/list/TAKE' A) n (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' A) (('const/rich_list/LASTN' A) n l)))))).
tt('thm/rich_list/SEG_REVERSE_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' ('const/arithmetic/+' n m) (('const/list/LENGTH' A) l)) => ((('const/rich_list/SEG' A) n m (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' A) (('const/rich_list/SEG' A) n ('const/arithmetic/-' (('const/list/LENGTH' A) l) ('const/arithmetic/+' n m)) l)))))).
tt('thm/rich_list/LENGTH_REPLICATE_', ax, ![A : $t]: (![n : 'type/num/num', x : A]: ((('const/list/LENGTH' A) (('const/rich_list/REPLICATE' A) n x)) = n))).
tt('thm/rich_list/MEM_REPLICATE_', ax, ![A : $t]: (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![x : A]: (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/rich_list/REPLICATE' A) n x))))))).
tt('thm/rich_list/AND_EL_FOLDL_', ax, (![l : ('type/list/list' $o)]: (('const/rich_list/AND_EL' l) = (('const/list/FOLDL' $o $o) $and $true l)))).
tt('thm/rich_list/AND_EL_FOLDR_', ax, (![l : ('type/list/list' $o)]: (('const/rich_list/AND_EL' l) = (('const/list/FOLDR' $o $o) $and $true l)))).
tt('thm/rich_list/OR_EL_FOLDL_', ax, (![l : ('type/list/list' $o)]: (('const/rich_list/OR_EL' l) = (('const/list/FOLDL' $o $o) $or $false l)))).
tt('thm/rich_list/OR_EL_FOLDR_', ax, (![l : ('type/list/list' $o)]: (('const/rich_list/OR_EL' l) = (('const/list/FOLDR' $o $o) $or $false l)))).
tt('thm/rich_list/IS_PREFIX_NIL_0', ax, ![A : $t]: (![x : ('type/list/list' A)]: (('const/list/isPREFIX' A) ('const/list/NIL' A) x))).
tt('thm/rich_list/IS_PREFIX_NIL_e1', ax, ![A : $t]: (![x : ('type/list/list' A)]: ((('const/list/isPREFIX' A) x ('const/list/NIL' A)) = (x = ('const/list/NIL' A))))).
tt('thm/rich_list/IS_PREFIX_REFL_', ax, ![A : $t]: (![x : ('type/list/list' A)]: (('const/list/isPREFIX' A) x x))).
tt('thm/rich_list/IS_PREFIX_ANTISYM_', ax, ![A : $t]: (![x : ('type/list/list' A), y : ('type/list/list' A)]: (((('const/list/isPREFIX' A) x y) & (('const/list/isPREFIX' A) y x)) => (x = y)))).
tt('thm/rich_list/IS_PREFIX_TRANS_', ax, ![A : $t]: (![x : ('type/list/list' A), y : ('type/list/list' A), z : ('type/list/list' A)]: (((('const/list/isPREFIX' A) y x) & (('const/list/isPREFIX' A) z y)) => (('const/list/isPREFIX' A) z x)))).
tt('thm/rich_list/IS_PREFIX_BUTLAST_', ax, ![A : $t]: (![x : A, y : ('type/list/list' A)]: (('const/list/isPREFIX' A) (('const/list/FRONT' A) (('const/list/CONS' A) x y)) (('const/list/CONS' A) x y)))).
tt('thm/rich_list/IS_PREFIX_LENGTH_', ax, ![A : $t]: (![x : ('type/list/list' A), y : ('type/list/list' A)]: ((('const/list/isPREFIX' A) x y) => ('const/arithmetic/<=' (('const/list/LENGTH' A) x) (('const/list/LENGTH' A) y))))).
tt('thm/rich_list/IS_PREFIX_LENGTH_ANTI_', ax, ![A : $t]: (![x : ('type/list/list' A), y : ('type/list/list' A)]: (((('const/list/isPREFIX' A) x y) & ((('const/list/LENGTH' A) x) = (('const/list/LENGTH' A) y))) = (x = y)))).
tt('thm/rich_list/IS_PREFIX_SNOC_', ax, ![A : $t]: (![x : A, y : ('type/list/list' A), z : ('type/list/list' A)]: ((('const/list/isPREFIX' A) z (('const/list/SNOC' A) x y)) = ((('const/list/isPREFIX' A) z y) | (z = (('const/list/SNOC' A) x y)))))).
tt('thm/rich_list/IS_PREFIX_APPEND1_', ax, ![A : $t]: (![a : ('type/list/list' A), b : ('type/list/list' A), c : ('type/list/list' A)]: ((('const/list/isPREFIX' A) (('const/list/APPEND' A) a b) c) => (('const/list/isPREFIX' A) a c)))).
tt('thm/rich_list/IS_PREFIX_APPEND2_', ax, ![A : $t]: (![a : ('type/list/list' A), b : ('type/list/list' A), c : ('type/list/list' A)]: ((('const/list/isPREFIX' A) a (('const/list/APPEND' A) b c)) => ((('const/list/isPREFIX' A) a b) | (('const/list/isPREFIX' A) b a))))).
tt('thm/rich_list/IS_PREFIX_APPENDS_', ax, ![A : $t]: (![a : ('type/list/list' A), b : ('type/list/list' A), c : ('type/list/list' A)]: ((('const/list/isPREFIX' A) (('const/list/APPEND' A) a b) (('const/list/APPEND' A) a c)) = (('const/list/isPREFIX' A) b c)))).
tt('thm/rich_list/IS_PREFIX_APPEND3_', ax, ![A : $t]: (![a : ('type/list/list' A), c : ('type/list/list' A)]: (('const/list/isPREFIX' A) a (('const/list/APPEND' A) a c)))).
tt('thm/rich_list/COUNT_LIST_GENLIST_', ax, (![n : 'type/num/num']: (('const/rich_list/COUNT_LIST' n) = (('const/list/GENLIST' 'type/num/num') ('const/combin/I' 'type/num/num') n)))).
tt('thm/rich_list/LENGTH_COUNT_LIST_', ax, (![n : 'type/num/num']: ((('const/list/LENGTH' 'type/num/num') ('const/rich_list/COUNT_LIST' n)) = n))).
tt('thm/rich_list/EL_COUNT_LIST_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) => ((('const/list/EL' 'type/num/num') m ('const/rich_list/COUNT_LIST' n)) = m)))).
tt('thm/rich_list/MEM_COUNT_LIST_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/bool/IN' 'type/num/num') m (('const/list/LIST_TO_SET' 'type/num/num') ('const/rich_list/COUNT_LIST' n))) = ('const/prim_rec/<' m n)))).
tt('thm/rich_list/COUNT_LIST_SNOC_0', ax, (('const/rich_list/COUNT_LIST' 'const/num/0') = ('const/list/NIL' 'type/num/num'))).
tt('thm/rich_list/COUNT_LIST_SNOC_e1', ax, (![n : 'type/num/num']: (('const/rich_list/COUNT_LIST' ('const/num/SUC' n)) = (('const/list/SNOC' 'type/num/num') n ('const/rich_list/COUNT_LIST' n))))).
tt('thm/rich_list/COUNT_LIST_COUNT_', ax, (![n : 'type/num/num']: ((('const/list/LIST_TO_SET' 'type/num/num') ('const/rich_list/COUNT_LIST' n)) = ('const/pred_set/count' n)))).
tt('thm/rich_list/COUNT_LIST_ADD_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/rich_list/COUNT_LIST' ('const/arithmetic/+' n m)) = (('const/list/APPEND' 'type/num/num') ('const/rich_list/COUNT_LIST' n) (('const/list/MAP' 'type/num/num' 'type/num/num') (^['n\'' : 'type/num/num']: ('const/arithmetic/+' 'n\'' n)) ('const/rich_list/COUNT_LIST' m)))))).
tt('thm/rich_list/EL_DROP_', ax, ![A : $t]: (![m : 'type/num/num', n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' ('const/arithmetic/+' m n) (('const/list/LENGTH' A) l)) => ((('const/list/EL' A) m (('const/list/DROP' A) n l)) = (('const/list/EL' A) ('const/arithmetic/+' m n) l))))).
tt('thm/rich_list/SNOC_EL_TAKE_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/list/SNOC' A) (('const/list/EL' A) n l) (('const/list/TAKE' A) n l)) = (('const/list/TAKE' A) ('const/num/SUC' n) l))))).
tt('thm/rich_list/ZIP_TAKE_LEQ_', ax, ![B : $t, A : $t]: (![n : 'type/num/num', a : ('type/list/list' A), b : ('type/list/list' B)]: ((('const/arithmetic/<=' n (('const/list/LENGTH' A) a)) & ('const/arithmetic/<=' (('const/list/LENGTH' A) a) (('const/list/LENGTH' B) b))) => ((('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/TAKE' A) n a) (('const/list/TAKE' B) n b))) = (('const/list/TAKE' ('type/pair/prod' A B)) n (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) a (('const/list/TAKE' B) (('const/list/LENGTH' A) a) b)))))))).
tt('thm/rich_list/ZIP_TAKE_', ax, ![B : $t, A : $t]: (![n : 'type/num/num', a : ('type/list/list' A), b : ('type/list/list' B)]: ((('const/arithmetic/<=' n (('const/list/LENGTH' A) a)) & ((('const/list/LENGTH' A) a) = (('const/list/LENGTH' B) b))) => ((('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/TAKE' A) n a) (('const/list/TAKE' B) n b))) = (('const/list/TAKE' ('type/pair/prod' A B)) n (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) a b))))))).
tt('thm/rich_list/EL_TAKE_', ax, ![A : $t]: (![n : 'type/num/num', x : 'type/num/num', l : ('type/list/list' A)]: ((('const/prim_rec/<' x n) & ('const/arithmetic/<=' n (('const/list/LENGTH' A) l))) => ((('const/list/EL' A) x (('const/list/TAKE' A) n l)) = (('const/list/EL' A) x l))))).
tt('thm/rich_list/ZIP_APPEND_', ax, ![B : $t, A : $t]: (![a : ('type/list/list' A), b : ('type/list/list' B), c : ('type/list/list' A), d : ('type/list/list' B)]: ((((('const/list/LENGTH' A) a) = (('const/list/LENGTH' B) b)) & ((('const/list/LENGTH' A) c) = (('const/list/LENGTH' B) d))) => ((('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) a b)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) c d))) = (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/APPEND' A) a c) (('const/list/APPEND' B) b d))))))).
tt('thm/rich_list/APPEND_ASSOC_CONS_', ax, ![A : $t]: (![l1 : ('type/list/list' A), h : A, l2 : ('type/list/list' A), l3 : ('type/list/list' A)]: ((('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) h l2)) l3) = (('const/list/APPEND' A) l1 (('const/list/CONS' A) h (('const/list/APPEND' A) l2 l3)))))).
tt('thm/rich_list/APPEND_SNOC1_', ax, ![A : $t]: (![l1 : ('type/list/list' A), x : A, l2 : ('type/list/list' A)]: ((('const/list/APPEND' A) (('const/list/SNOC' A) x l1) l2) = (('const/list/APPEND' A) l1 (('const/list/CONS' A) x l2))))).
tt('thm/rich_list/FOLDL_MAP2_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > (B > A)), e : A, g : (C > B), l : ('type/list/list' C)]: ((('const/list/FOLDL' B A) f e (('const/list/MAP' C B) g l)) = (('const/list/FOLDL' C A) (^[x : A, y : C]: (f x (g y))) e l)))).
tt('thm/rich_list/SPLITP_EVERY_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) (^[x : A]: (~ (P x))) l) => ((('const/rich_list/SPLITP' A) P l) = (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) l ('const/list/NIL' A)))))).
tt('thm/rich_list/MEM_FRONT_', ax, ![A : $t]: (![l : ('type/list/list' A), e : A, y : A]: ((('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) (('const/list/FRONT' A) (('const/list/CONS' A) e l)))) => (('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) (('const/list/CONS' A) e l)))))).
tt('thm/rich_list/FRONT_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), e : A]: ((('const/list/FRONT' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) e l2))) = (('const/list/APPEND' A) l1 (('const/list/FRONT' A) (('const/list/CONS' A) e l2)))))).
tt('thm/rich_list/EL_FRONT_', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: ((('const/prim_rec/<' n (('const/list/LENGTH' A) (('const/list/FRONT' A) l))) & (~ (('const/list/NULL' A) l))) => ((('const/list/EL' A) n (('const/list/FRONT' A) l)) = (('const/list/EL' A) n l))))).
tt('thm/rich_list/MEM_LAST_', ax, ![A : $t]: (![e : A, l : ('type/list/list' A)]: (('const/bool/IN' A) (('const/list/LAST' A) (('const/list/CONS' A) e l)) (('const/list/LIST_TO_SET' A) (('const/list/CONS' A) e l))))).
tt('thm/rich_list/DROP_CONS_EL_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => ((('const/list/DROP' A) n l) = (('const/list/CONS' A) (('const/list/EL' A) n l) (('const/list/DROP' A) ('const/num/SUC' n) l)))))).
tt('thm/rich_list/MEM_LAST_FRONT_', ax, ![A : $t]: (![e : A, l : ('type/list/list' A), h : A]: (((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)) & (~ (e = (('const/list/LAST' A) (('const/list/CONS' A) h l))))) => (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) (('const/list/FRONT' A) (('const/list/CONS' A) h l))))))).
tt('thm/rich_list/LIST_ELEM_COUNT_THM_0', ax, ![A : $t]: (![e : A]: ((('const/rich_list/LIST_ELEM_COUNT' A) e ('const/list/NIL' A)) = 'const/num/0'))).
tt('thm/rich_list/LIST_ELEM_COUNT_THM_1', ax, ![B : $t]: (![e : B, l1 : ('type/list/list' B), l2 : ('type/list/list' B)]: ((('const/rich_list/LIST_ELEM_COUNT' B) e (('const/list/APPEND' B) l1 l2)) = ('const/arithmetic/+' (('const/rich_list/LIST_ELEM_COUNT' B) e l1) (('const/rich_list/LIST_ELEM_COUNT' B) e l2))))).
tt('thm/rich_list/LIST_ELEM_COUNT_THM_2', ax, ![C : $t]: (![e : C, h : C, l : ('type/list/list' C)]: ((h = e) => ((('const/rich_list/LIST_ELEM_COUNT' C) e (('const/list/CONS' C) h l)) = ('const/num/SUC' (('const/rich_list/LIST_ELEM_COUNT' C) e l)))))).
tt('thm/rich_list/LIST_ELEM_COUNT_THM_e3', ax, ![D : $t]: (![e : D, h : D, l : ('type/list/list' D)]: ((~ (h = e)) => ((('const/rich_list/LIST_ELEM_COUNT' D) e (('const/list/CONS' D) h l)) = (('const/rich_list/LIST_ELEM_COUNT' D) e l))))).
tt('thm/rich_list/LIST_ELEM_COUNT_MEM_', ax, ![A : $t]: (![e : A, l : ('type/list/list' A)]: (('const/arithmetic/>' (('const/rich_list/LIST_ELEM_COUNT' A) e l) 'const/num/0') = (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l))))).
tt('thm/rich_list/LIST_TO_SET_EQ_SING_', ax, ![A : $t]: (![x : A, ls : ('type/list/list' A)]: (((('const/list/LIST_TO_SET' A) ls) = (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) = ((~ (ls = ('const/list/NIL' A))) & (('const/list/EVERY' A) (($equals A) x) ls))))).
tt('thm/rich_list/REPLICATE_GENLIST_', ax, ![A : $t]: (![n : 'type/num/num', x : A]: ((('const/rich_list/REPLICATE' A) n x) = (('const/list/GENLIST' A) (('const/combin/K' A 'type/num/num') x) n)))).
tt('thm/rich_list/EL_REPLICATE_', ax, ![A : $t]: (![n1 : 'type/num/num', n2 : 'type/num/num', x : A]: (('const/prim_rec/<' n1 n2) => ((('const/list/EL' A) n1 (('const/rich_list/REPLICATE' A) n2 x)) = x)))).
tt('thm/rich_list/EVERY_REPLICATE_', ax, ![A : $t]: (![f : (A > $o), n : 'type/num/num', x : A]: ((('const/list/EVERY' A) f (('const/rich_list/REPLICATE' A) n x)) = ((n = 'const/num/0') | (f x))))).
tt('thm/rich_list/ALL_DISTINCT_DROP_', ax, ![A : $t]: (![ls : ('type/list/list' A), n : 'type/num/num']: ((('const/list/ALL_DISTINCT' A) ls) => (('const/list/ALL_DISTINCT' A) (('const/list/DROP' A) n ls))))).
tt('thm/rich_list/MAP_SND_FILTER_NEQ_', ax, ![B : $t, A : $t]: (![z : A, ls : ('type/list/list' ('type/pair/prod' B A))]: ((('const/list/MAP' ('type/pair/prod' B A) A) ('const/pair/SND' B A) (('const/list/FILTER' ('type/pair/prod' B A)) (('const/pair/UNCURRY' B A $o) (^[x : B, y : A]: (~ (y = z)))) ls)) = (('const/list/FILTER' A) (^[y : A]: (~ (z = y))) (('const/list/MAP' ('type/pair/prod' B A) A) ('const/pair/SND' B A) ls))))).
tt('thm/rich_list/MEM_SING_APPEND_', ax, ![A : $t]: (![d : ('type/list/list' A), b : A]: ((![a : ('type/list/list' A), c : ('type/list/list' A)]: (~ (d = (('const/list/APPEND' A) (('const/list/APPEND' A) a (('const/list/CONS' A) b ('const/list/NIL' A))) c)))) = (~ (('const/bool/IN' A) b (('const/list/LIST_TO_SET' A) d)))))).
tt('thm/rich_list/EL_LENGTH_APPEND_rwt_', ax, ![A : $t]: (![n : 'type/num/num', l2 : ('type/list/list' A), l1 : ('type/list/list' A)]: (((~ (('const/list/NULL' A) l2)) & (n = (('const/list/LENGTH' A) l1))) => ((('const/list/EL' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/HD' A) l2))))).
tt('thm/rich_list/MAP_FST_funs_', ax, ![A : $t, B : $t, C : $t]: (![funs : ('type/list/list' ('type/pair/prod' A ('type/pair/prod' B C)))]: ((('const/list/MAP' ('type/pair/prod' A ('type/pair/prod' B C)) A) (('const/pair/UNCURRY' A ('type/pair/prod' B C) A) (^[x : A]: (('const/pair/UNCURRY' B C A) (^[y : B, z : C]: x)))) funs) = (('const/list/MAP' ('type/pair/prod' A ('type/pair/prod' B C)) A) ('const/pair/FST' A ('type/pair/prod' B C)) funs)))).
tt('thm/rich_list/TAKE_PRE_LENGTH_', ax, ![A : $t]: (![ls : ('type/list/list' A)]: ((~ (ls = ('const/list/NIL' A))) => ((('const/list/TAKE' A) ('const/prim_rec/PRE' (('const/list/LENGTH' A) ls)) ls) = (('const/list/FRONT' A) ls))))).
tt('thm/rich_list/DROP_LENGTH_NIL_rwt_', ax, ![A : $t]: (![l : ('type/list/list' A), m : 'type/num/num']: ((m = (('const/list/LENGTH' A) l)) => ((('const/list/DROP' A) m l) = ('const/list/NIL' A))))).
tt('thm/rich_list/DROP_EL_CONS_', ax, ![A : $t]: (![ls : ('type/list/list' A), n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) ls)) => ((('const/list/DROP' A) n ls) = (('const/list/CONS' A) (('const/list/EL' A) n ls) (('const/list/DROP' A) ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ls)))))).
tt('thm/rich_list/TAKE_EL_SNOC_', ax, ![A : $t]: (![ls : ('type/list/list' A), n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) ls)) => ((('const/list/TAKE' A) ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ls) = (('const/list/SNOC' A) (('const/list/EL' A) n ls) (('const/list/TAKE' A) n ls)))))).
tt('thm/rich_list/EVERY2_DROP_', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), l1 : ('type/list/list' A), l2 : ('type/list/list' B), n : 'type/num/num']: (((('const/list/LIST_REL' A B) R l1 l2) & ('const/arithmetic/<=' n (('const/list/LENGTH' A) l1))) => (('const/list/LIST_REL' A B) R (('const/list/DROP' A) n l1) (('const/list/DROP' B) n l2))))).
tt('thm/rich_list/REVERSE_DROP_', ax, ![A : $t]: (![ls : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' n (('const/list/LENGTH' A) ls)) => ((('const/list/REVERSE' A) (('const/list/DROP' A) n ls)) = (('const/list/REVERSE' A) (('const/rich_list/LASTN' A) ('const/arithmetic/-' (('const/list/LENGTH' A) ls) n) ls)))))).
tt('thm/rich_list/LENGTH_FILTER_LESS_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A)]: ((('const/list/EXISTS' A) (('const/combin/o' A $o $o) $not P) ls) => ('const/prim_rec/<' (('const/list/LENGTH' A) (('const/list/FILTER' A) P ls)) (('const/list/LENGTH' A) ls))))).
tt('thm/rich_list/EVERY2_APPEND_', ax, ![B : $t, A : $t]: (![l4 : ('type/list/list' B), l3 : ('type/list/list' A), l2 : ('type/list/list' B), l1 : ('type/list/list' A), R : (A > (B > $o))]: (((('const/list/LIST_REL' A B) R l1 l2) & (('const/list/LIST_REL' A B) R l3 l4)) = ((('const/list/LIST_REL' A B) R (('const/list/APPEND' A) l1 l3) (('const/list/APPEND' B) l2 l4)) & (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) & ((('const/list/LENGTH' A) l3) = (('const/list/LENGTH' B) l4))))))).
tt('thm/rich_list/EVERY2_APPEND_suff_', ax, ![B : $t, A : $t]: (![l4 : ('type/list/list' B), l3 : ('type/list/list' A), l2 : ('type/list/list' B), l1 : ('type/list/list' A), R : (A > (B > $o))]: (((('const/list/LIST_REL' A B) R l1 l2) & (('const/list/LIST_REL' A B) R l3 l4)) => (('const/list/LIST_REL' A B) R (('const/list/APPEND' A) l1 l3) (('const/list/APPEND' B) l2 l4))))).
tt('thm/rich_list/LIST_REL_APPEND_SING_', ax, ![B : $t, A : $t]: (![x2 : B, x1 : A, l2 : ('type/list/list' B), l1 : ('type/list/list' A), R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R (('const/list/APPEND' A) l1 (('const/list/CONS' A) x1 ('const/list/NIL' A))) (('const/list/APPEND' B) l2 (('const/list/CONS' B) x2 ('const/list/NIL' B)))) = ((('const/list/LIST_REL' A B) R l1 l2) & (R x1 x2))))).
tt('thm/rich_list/ALL_DISTINCT_MEM_ZIP_MAP_', ax, ![A : $t, B : $t]: (![f : (A > B), x : ('type/pair/prod' A B), ls : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) ls) => ((('const/bool/IN' ('type/pair/prod' A B)) x (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) ls (('const/list/MAP' A B) f ls))))) = ((('const/bool/IN' A) (('const/pair/FST' A B) x) (('const/list/LIST_TO_SET' A) ls)) & ((('const/pair/SND' A B) x) = (f (('const/pair/FST' A B) x)))))))).
tt('thm/rich_list/REVERSE_ZIP_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => ((('const/list/REVERSE' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/REVERSE' A) l1) (('const/list/REVERSE' B) l2))))))).
tt('thm/rich_list/EVERY2_REVERSE1_', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) R l1 (('const/list/REVERSE' B) l2)) = (('const/list/LIST_REL' A B) R (('const/list/REVERSE' A) l1) l2)))).
tt('thm/rich_list/every_count_list_', ax, (![P : ('type/num/num' > $o), n : 'type/num/num']: ((('const/list/EVERY' 'type/num/num') P ('const/rich_list/COUNT_LIST' n)) = (![m : 'type/num/num']: (('const/prim_rec/<' m n) => (P m)))))).
tt('thm/rich_list/count_list_sub1_', ax, (![n : 'type/num/num']: ((~ (n = 'const/num/0')) => (('const/rich_list/COUNT_LIST' n) = (('const/list/CONS' 'type/num/num') 'const/num/0' (('const/list/MAP' 'type/num/num' 'type/num/num') 'const/num/SUC' ('const/rich_list/COUNT_LIST' ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))).
tt('thm/rich_list/el_map_count_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A), m : 'type/num/num']: (('const/prim_rec/<' n m) => ((('const/list/EL' A) n (('const/list/MAP' 'type/num/num' A) f ('const/rich_list/COUNT_LIST' m))) = (f n))))).
tt('thm/rich_list/ZIP_COUNT_LIST_', ax, ![A : $t]: (![n : 'type/num/num', l1 : ('type/list/list' A)]: ((n = (('const/list/LENGTH' A) l1)) => ((('const/list/ZIP' A 'type/num/num') (('const/pair/,' ('type/list/list' A) ('type/list/list' 'type/num/num')) l1 ('const/rich_list/COUNT_LIST' n))) = (('const/list/GENLIST' ('type/pair/prod' A 'type/num/num')) (^[n0 : 'type/num/num']: (('const/pair/,' A 'type/num/num') (('const/list/EL' A) n0 l1) n0)) (('const/list/LENGTH' A) l1)))))).
tt('thm/rich_list/map_replicate_', ax, ![A : $t, B : $t]: (![f : (A > B), n : 'type/num/num', x : A]: ((('const/list/MAP' A B) f (('const/rich_list/REPLICATE' A) n x)) = (('const/rich_list/REPLICATE' B) n (f x))))).
tt('thm/rich_list/take_drop_partition_', ax, ![A : $t]: (![n : 'type/num/num', m : 'type/num/num', l : ('type/list/list' A)]: (('const/arithmetic/<=' m n) => ((('const/list/APPEND' A) (('const/list/TAKE' A) m l) (('const/list/TAKE' A) ('const/arithmetic/-' n m) (('const/list/DROP' A) m l))) = (('const/list/TAKE' A) n l))))).
tt('thm/rich_list/all_distinct_count_list_', ax, (![n : 'type/num/num']: (('const/list/ALL_DISTINCT' 'type/num/num') ('const/rich_list/COUNT_LIST' n)))).
tt('thm/rich_list/COUNT_LIST_compute_', ax, (![n : 'type/num/num']: (('const/rich_list/COUNT_LIST' n) = ('const/rich_list/COUNT_LIST_AUX' n ('const/list/NIL' 'type/num/num'))))).
tt('thm/rich_list/SPLITP_compute_', ax, ![A : $t]: (('const/rich_list/SPLITP' A) = (('const/rich_list/SPLITP_AUX' A) ('const/list/NIL' A)))).
tt('thm/rich_list/IS_SUFFIX_compute_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/rich_list/IS_SUFFIX' A) l1 l2) = (('const/list/isPREFIX' A) (('const/list/REVERSE' A) l2) (('const/list/REVERSE' A) l1))))).
tt('thm/rich_list/SEG_compute_0', ax, ![A : $t]: (![k : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) 'const/num/0' k l) = ('const/list/NIL' A)))).
tt('thm/rich_list/SEG_compute_1', ax, ![A : $t]: (![m : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) 'const/num/0' (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/rich_list/SEG' A) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) 'const/num/0' l))))).
tt('thm/rich_list/SEG_compute_2', ax, ![A : $t]: (![m : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) 'const/num/0' (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) 'const/num/0' l))))).
tt('thm/rich_list/SEG_compute_3', ax, ![A : $t]: (![m : 'type/num/num', k : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' k)) (('const/list/CONS' A) x l)) = (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' k)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) l)))).
tt('thm/rich_list/SEG_compute_4', ax, ![A : $t]: (![m : 'type/num/num', k : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' k)) (('const/list/CONS' A) x l)) = (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' k)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) l)))).
tt('thm/rich_list/SEG_compute_5', ax, ![A : $t]: (![m : 'type/num/num', k : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' k)) (('const/list/CONS' A) x l)) = (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' k)) l)))).
tt('thm/rich_list/SEG_compute_e6', ax, ![A : $t]: (![m : 'type/num/num', k : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' k)) (('const/list/CONS' A) x l)) = (('const/rich_list/SEG' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' k)) l)))).
tt('thm/rich_list/BUTLASTN_compute_', ax, ![A : $t]: (!['longer than list' : $o, n : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/BUTLASTN' A) n l) = (('const/bool/LET' 'type/num/num' ('type/list/list' A)) (^[m : 'type/num/num']: (('const/bool/COND' ('type/list/list' A)) ('const/arithmetic/<=' n m) (('const/list/TAKE' A) ('const/arithmetic/-' m n) l) (('const/combin/FAIL' ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))) $o) ('const/rich_list/BUTLASTN' A) 'longer than list' n l))) (('const/list/LENGTH' A) l))))).
tt('thm/rich_list/LASTN_compute_', ax, ![A : $t]: (!['longer than list' : $o, n : 'type/num/num', l : ('type/list/list' A)]: ((('const/rich_list/LASTN' A) n l) = (('const/bool/LET' 'type/num/num' ('type/list/list' A)) (^[m : 'type/num/num']: (('const/bool/COND' ('type/list/list' A)) ('const/arithmetic/<=' n m) (('const/list/DROP' A) ('const/arithmetic/-' m n) l) (('const/combin/FAIL' ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))) $o) ('const/rich_list/LASTN' A) 'longer than list' n l))) (('const/list/LENGTH' A) l))))).
