tt('type/list/list', ty, $t > $t).
tt('const/list/ALL_DISTINCT', ty, ![A : $t]: (('type/list/list' A) > $o)).
tt('const/list/APPEND', ty, ![A : $t]: (('type/list/list' A) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/CONS', ty, ![A : $t]: (A > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/DROP', ty, ![A : $t]: ('type/num/num' > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/EL', ty, ![A : $t]: ('type/num/num' > (('type/list/list' A) > A))).
tt('const/list/EVERY', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > $o))).
tt('const/list/EVERYi', ty, ![A : $t]: (('type/num/num' > (A > $o)) > (('type/list/list' A) > $o))).
tt('const/list/EXISTS', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > $o))).
tt('const/list/FILTER', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/FIND', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/option/option' A)))).
tt('const/list/FLAT', ty, ![A : $t]: (('type/list/list' ('type/list/list' A)) > ('type/list/list' A))).
tt('const/list/FOLDL', ty, ![A : $t, B : $t]: ((B > (A > B)) > (B > (('type/list/list' A) > B)))).
tt('const/list/FOLDL2', ty, ![A : $t, B : $t, C : $t]: ((A > (B > (C > A))) > (A > (('type/list/list' B) > (('type/list/list' C) > A))))).
tt('const/list/FOLDR', ty, ![A : $t, B : $t]: ((A > (B > B)) > (B > (('type/list/list' A) > B)))).
tt('const/list/FRONT', ty, ![A : $t]: (('type/list/list' A) > ('type/list/list' A))).
tt('const/list/GENLIST', ty, ![A : $t]: (('type/num/num' > A) > ('type/num/num' > ('type/list/list' A)))).
tt('const/list/GENLIST_AUX', ty, ![A : $t]: (('type/num/num' > A) > ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/list/HD', ty, ![A : $t]: (('type/list/list' A) > A)).
tt('const/list/INDEX_FIND', ty, ![A : $t]: ('type/num/num' > ((A > $o) > (('type/list/list' A) > ('type/option/option' ('type/pair/prod' 'type/num/num' A)))))).
tt('const/list/INDEX_OF', ty, ![A : $t]: (A > (('type/list/list' A) > ('type/option/option' 'type/num/num')))).
tt('const/list/LAST', ty, ![A : $t]: (('type/list/list' A) > A)).
tt('const/list/LEN', ty, ![A : $t]: (('type/list/list' A) > ('type/num/num' > 'type/num/num'))).
tt('const/list/LENGTH', ty, ![A : $t]: (('type/list/list' A) > 'type/num/num')).
tt('const/list/LIST_APPLY', ty, ![A : $t, B : $t]: (('type/list/list' (B > A)) > (('type/list/list' B) > ('type/list/list' A)))).
tt('const/list/LIST_BIND', ty, ![A : $t, B : $t]: (('type/list/list' B) > ((B > ('type/list/list' A)) > ('type/list/list' A)))).
tt('const/list/LIST_IGNORE_BIND', ty, ![A : $t, B : $t]: (('type/list/list' B) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/LIST_LIFT2', ty, ![A : $t, B : $t, C : $t]: ((B > (C > A)) > (('type/list/list' B) > (('type/list/list' C) > ('type/list/list' A))))).
tt('const/list/LIST_REL', ty, ![A : $t, B : $t]: ((A > (B > $o)) > (('type/list/list' A) > (('type/list/list' B) > $o)))).
tt('const/list/LIST_TO_SET', ty, ![A : $t]: (('type/list/list' A) > (A > $o))).
tt('const/list/LLEX', ty, ![A : $t]: ((A > (A > $o)) > (('type/list/list' A) > (('type/list/list' A) > $o)))).
tt('const/list/LRC', ty, ![A : $t]: ((A > (A > $o)) > (('type/list/list' A) > (A > (A > $o))))).
tt('const/list/LUPDATE', ty, ![A : $t]: (A > ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/list/MAP', ty, ![A : $t, B : $t]: ((A > B) > (('type/list/list' A) > ('type/list/list' B)))).
tt('const/list/MAP2', ty, ![A : $t, B : $t, C : $t]: ((B > (C > A)) > (('type/list/list' B) > (('type/list/list' C) > ('type/list/list' A))))).
tt('const/list/NIL', ty, ![A : $t]: ('type/list/list' A)).
tt('const/list/NULL', ty, ![A : $t]: (('type/list/list' A) > $o)).
tt('const/list/PAD_LEFT', ty, ![A : $t]: (A > ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/list/PAD_RIGHT', ty, ![A : $t]: (A > ('type/num/num' > (('type/list/list' A) > ('type/list/list' A))))).
tt('const/list/REV', ty, ![A : $t]: (('type/list/list' A) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/REVERSE', ty, ![A : $t]: (('type/list/list' A) > ('type/list/list' A))).
tt('const/list/SET_TO_LIST', ty, ![A : $t]: ((A > $o) > ('type/list/list' A))).
tt('const/list/SNOC', ty, ![A : $t]: (A > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/SUM', ty, (('type/list/list' 'type/num/num') > 'type/num/num')).
tt('const/list/SUM_ACC', ty, (('type/list/list' 'type/num/num') > ('type/num/num' > 'type/num/num'))).
tt('const/list/TAKE', ty, ![A : $t]: ('type/num/num' > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/TL', ty, ![A : $t]: (('type/list/list' A) > ('type/list/list' A))).
tt('const/list/UNZIP', ty, ![A : $t, B : $t]: (('type/list/list' ('type/pair/prod' A B)) > ('type/pair/prod' ('type/list/list' A) ('type/list/list' B)))).
tt('const/list/ZIP', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/list/list' A) ('type/list/list' B)) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/list/dropWhile', ty, ![A : $t]: ((A > $o) > (('type/list/list' A) > ('type/list/list' A)))).
tt('const/list/isPREFIX', ty, ![A : $t]: (('type/list/list' A) > (('type/list/list' A) > $o))).
tt('const/list/list_CASE', ty, ![A : $t, B : $t]: (('type/list/list' A) > (B > ((A > (('type/list/list' A) > B)) > B)))).
tt('const/list/list_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/list/list' A) > 'type/num/num'))).
tt('const/list/nub', ty, ![A : $t]: (('type/list/list' A) > ('type/list/list' A))).
tt('const/list/splitAtPki', ty, ![A : $t, B : $t]: (('type/num/num' > (B > $o)) > ((('type/list/list' B) > (('type/list/list' B) > A)) > (('type/list/list' B) > A)))).
tt('thm/list/list_TY_DEF_', def, ![A : $t]: (?[rep : (('type/list/list' A) > ('type/ind_type/recspace' A))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' A) ('type/list/list' A)) (^['a0\'' : ('type/ind_type/recspace' A)]: (!['\'list\'' : (('type/ind_type/recspace' A) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' A)]: ((('a0\'0' = (('const/ind_type/CONSTR' A) 'const/num/0' ('const/bool/ARB' A) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))) | (?[a0 : A, a1 : ('type/ind_type/recspace' A)]: (('a0\'0' = ((^[a00 : A, a10 : ('type/ind_type/recspace' A)]: (('const/ind_type/CONSTR' A) ('const/num/SUC' 'const/num/0') a00 (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a10 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A))))) a0 a1)) & ('\'list\'' a1)))) => ('\'list\'' 'a0\'0'))) => ('\'list\'' 'a0\'')))) rep))).
tt('thm/list/list_case_def_0', def, ![B : $t, A : $t]: (![v : B, f : (A > (('type/list/list' A) > B))]: ((('const/list/list_CASE' A B) ('const/list/NIL' A) v f) = v))).
tt('thm/list/list_case_def_e1', def, ![A : $t, B : $t]: (![a0 : A, a1 : ('type/list/list' A), v : B, f : (A > (('type/list/list' A) > B))]: ((('const/list/list_CASE' A B) (('const/list/CONS' A) a0 a1) v f) = (f a0 a1)))).
tt('thm/list/list_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/list/list_size' A) f ('const/list/NIL' A)) = 'const/num/0'))).
tt('thm/list/list_size_def_e1', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : A, a1 : ('type/list/list' A)]: ((('const/list/list_size' A) f (('const/list/CONS' A) a0 a1)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (f a0) (('const/list/list_size' A) f a1)))))).
tt('thm/list/datatype_list_', ax, ![A : $t]: (![list : (('type/list/list' A) > ((A > (('type/list/list' A) > ('type/list/list' A))) > $o))]: (('const/bool/DATATYPE' $o) (list ('const/list/NIL' A) ('const/list/CONS' A))))).
tt('thm/list/list_11_', ax, ![A : $t]: (![a0 : A, a1 : ('type/list/list' A), 'a0\'' : A, 'a1\'' : ('type/list/list' A)]: (((('const/list/CONS' A) a0 a1) = (('const/list/CONS' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/list/list_distinct_', ax, ![A : $t]: (![a1 : ('type/list/list' A), a0 : A]: (~ (('const/list/NIL' A) = (('const/list/CONS' A) a0 a1))))).
tt('thm/list/list_case_cong_', ax, ![A : $t, B : $t]: (!['v\'' : B, 'f\'' : (A > (('type/list/list' A) > B)), M : ('type/list/list' A), 'M\'' : ('type/list/list' A), v : B, f : (A > (('type/list/list' A) > B))]: (((M = 'M\'') & ((('M\'' = ('const/list/NIL' A)) => (v = 'v\'')) & (![a0 : A, a1 : ('type/list/list' A)]: (('M\'' = (('const/list/CONS' A) a0 a1)) => ((f a0 a1) = ('f\'' a0 a1)))))) => ((('const/list/list_CASE' A B) M v f) = (('const/list/list_CASE' A B) 'M\'' 'v\'' 'f\''))))).
tt('thm/list/list_Axiom_', ax, ![A : $t, B : $t]: (![f0 : B, f1 : (A > (('type/list/list' A) > (B > B)))]: (?[fn : (('type/list/list' A) > B)]: (((fn ('const/list/NIL' A)) = f0) & (![a0 : A, a1 : ('type/list/list' A)]: ((fn (('const/list/CONS' A) a0 a1)) = (f1 a0 a1 (fn a1)))))))).
tt('thm/list/list_Axiom_old_', ax, ![A : $t, B : $t]: (![x : B, f : (B > (A > (('type/list/list' A) > B)))]: (('const/bool/?!' (('type/list/list' A) > B)) (^[fn1 : (('type/list/list' A) > B)]: (((fn1 ('const/list/NIL' A)) = x) & (![h : A, t : ('type/list/list' A)]: ((fn1 (('const/list/CONS' A) h t)) = (f (fn1 t) h t)))))))).
tt('thm/list/NULL_DEF_0', def, ![A : $t]: ((('const/list/NULL' A) ('const/list/NIL' A)) = $true)).
tt('thm/list/NULL_DEF_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/NULL' A) (('const/list/CONS' A) h t)) = $false))).
tt('thm/list/HD_', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/HD' A) (('const/list/CONS' A) h t)) = h))).
tt('thm/list/TL_', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/TL' A) (('const/list/CONS' A) h t)) = t))).
tt('thm/list/SUM_0', def, (('const/list/SUM' ('const/list/NIL' 'type/num/num')) = 'const/num/0')).
tt('thm/list/SUM_e1', def, (![h : 'type/num/num', t : ('type/list/list' 'type/num/num')]: (('const/list/SUM' (('const/list/CONS' 'type/num/num') h t)) = ('const/arithmetic/+' h ('const/list/SUM' t))))).
tt('thm/list/APPEND_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/APPEND' A) ('const/list/NIL' A) l) = l))).
tt('thm/list/APPEND_e1', def, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), h : A]: ((('const/list/APPEND' A) (('const/list/CONS' A) h l1) l2) = (('const/list/CONS' A) h (('const/list/APPEND' A) l1 l2))))).
tt('thm/list/FLAT_0', def, ![A : $t]: ((('const/list/FLAT' A) ('const/list/NIL' ('type/list/list' A))) = ('const/list/NIL' A))).
tt('thm/list/FLAT_e1', def, ![A : $t]: (![h : ('type/list/list' A), t : ('type/list/list' ('type/list/list' A))]: ((('const/list/FLAT' A) (('const/list/CONS' ('type/list/list' A)) h t)) = (('const/list/APPEND' A) h (('const/list/FLAT' A) t))))).
tt('thm/list/LENGTH_0', def, ![A : $t]: ((('const/list/LENGTH' A) ('const/list/NIL' A)) = 'const/num/0')).
tt('thm/list/LENGTH_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/CONS' A) h t)) = ('const/num/SUC' (('const/list/LENGTH' A) t))))).
tt('thm/list/MAP_0', def, ![B : $t, A : $t]: (![f : (A > B)]: ((('const/list/MAP' A B) f ('const/list/NIL' A)) = ('const/list/NIL' B)))).
tt('thm/list/MAP_e1', def, ![A : $t, B : $t]: (![f : (A > B), h : A, t : ('type/list/list' A)]: ((('const/list/MAP' A B) f (('const/list/CONS' A) h t)) = (('const/list/CONS' B) (f h) (('const/list/MAP' A B) f t))))).
tt('thm/list/LIST_TO_SET_DEF_0', def, ![A : $t]: (![x : A]: ((('const/list/LIST_TO_SET' A) ('const/list/NIL' A) x) = $false))).
tt('thm/list/LIST_TO_SET_DEF_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A), x : A]: ((('const/list/LIST_TO_SET' A) (('const/list/CONS' A) h t) x) = ((x = h) | (('const/list/LIST_TO_SET' A) t x))))).
tt('thm/list/LIST_TO_SET_0', ax, ![A : $t]: ((('const/list/LIST_TO_SET' A) ('const/list/NIL' A)) = ('const/pred_set/EMPTY' A))).
tt('thm/list/LIST_TO_SET_e1', ax, ![B : $t]: (![t : ('type/list/list' B), h : B]: ((('const/list/LIST_TO_SET' B) (('const/list/CONS' B) h t)) = (('const/pred_set/INSERT' B) h (('const/list/LIST_TO_SET' B) t))))).
tt('thm/list/IN_LIST_TO_SET_', ax, $true).
tt('thm/list/FILTER_0', def, ![A : $t]: (![P : (A > $o)]: ((('const/list/FILTER' A) P ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/FILTER_e1', def, ![A : $t]: (![P : (A > $o), h : A, t : ('type/list/list' A)]: ((('const/list/FILTER' A) P (('const/list/CONS' A) h t)) = (('const/bool/COND' ('type/list/list' A)) (P h) (('const/list/CONS' A) h (('const/list/FILTER' A) P t)) (('const/list/FILTER' A) P t))))).
tt('thm/list/FOLDR_0', def, ![B : $t, A : $t]: (![f : (A > (B > B)), e : B]: ((('const/list/FOLDR' A B) f e ('const/list/NIL' A)) = e))).
tt('thm/list/FOLDR_e1', def, ![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/CONS' A) x l)) = (f x (('const/list/FOLDR' A B) f e l))))).
tt('thm/list/FOLDL_0', def, ![B : $t, A : $t]: (![f : (B > (A > B)), e : B]: ((('const/list/FOLDL' A B) f e ('const/list/NIL' A)) = e))).
tt('thm/list/FOLDL_e1', def, ![A : $t, B : $t]: (![f : (B > (A > B)), e : B, x : A, l : ('type/list/list' A)]: ((('const/list/FOLDL' A B) f e (('const/list/CONS' A) x l)) = (('const/list/FOLDL' A B) f (f e x) l)))).
tt('thm/list/EVERY_DEF_0', def, ![A : $t]: (![P : (A > $o)]: ((('const/list/EVERY' A) P ('const/list/NIL' A)) = $true))).
tt('thm/list/EVERY_DEF_e1', def, ![A : $t]: (![P : (A > $o), h : A, t : ('type/list/list' A)]: ((('const/list/EVERY' A) P (('const/list/CONS' A) h t)) = ((P h) & (('const/list/EVERY' A) P t))))).
tt('thm/list/EXISTS_DEF_0', def, ![A : $t]: (![P : (A > $o)]: ((('const/list/EXISTS' A) P ('const/list/NIL' A)) = $false))).
tt('thm/list/EXISTS_DEF_e1', def, ![A : $t]: (![P : (A > $o), h : A, t : ('type/list/list' A)]: ((('const/list/EXISTS' A) P (('const/list/CONS' A) h t)) = ((P h) | (('const/list/EXISTS' A) P t))))).
tt('thm/list/EL_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/EL' A) 'const/num/0' l) = (('const/list/HD' A) l)))).
tt('thm/list/EL_e1', def, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: ((('const/list/EL' A) ('const/num/SUC' n) l) = (('const/list/EL' A) n (('const/list/TL' A) l))))).
tt('thm/list/MAP2_ind_', ax, ![C : $t, B : $t, A : $t]: (![P : ((B > (C > A)) > (('type/list/list' B) > (('type/list/list' C) > $o)))]: (((![f : (B > (C > A)), h1 : B, t1 : ('type/list/list' B), h2 : C, t2 : ('type/list/list' C)]: ((P f t1 t2) => (P f (('const/list/CONS' B) h1 t1) (('const/list/CONS' C) h2 t2)))) & ((![f : (B > (C > A)), y : ('type/list/list' C)]: (P f ('const/list/NIL' B) y)) & (![f : (B > (C > A)), v4 : B, v5 : ('type/list/list' B)]: (P f (('const/list/CONS' B) v4 v5) ('const/list/NIL' C))))) => (![v : (B > (C > A)), v1 : ('type/list/list' B), v2 : ('type/list/list' C)]: (P v v1 v2))))).
tt('thm/list/MAP2_def_0', ax, ![C : $t, B : $t, A : $t]: (![t2 : ('type/list/list' C), t1 : ('type/list/list' B), h2 : C, h1 : B, f : (B > (C > A))]: ((('const/list/MAP2' A B C) f (('const/list/CONS' B) h1 t1) (('const/list/CONS' C) h2 t2)) = (('const/list/CONS' A) (f h1 h2) (('const/list/MAP2' A B C) f t1 t2))))).
tt('thm/list/MAP2_def_1', ax, ![A : $t, C : $t, B : $t]: (![y : ('type/list/list' C), f : (B > (C > A))]: ((('const/list/MAP2' A B C) f ('const/list/NIL' B) y) = ('const/list/NIL' A)))).
tt('thm/list/MAP2_def_e2', ax, ![A : $t, C : $t, B : $t]: (![v5 : ('type/list/list' B), v4 : B, f : (B > (C > A))]: ((('const/list/MAP2' A B C) f (('const/list/CONS' B) v4 v5) ('const/list/NIL' C)) = ('const/list/NIL' A)))).
tt('thm/list/MAP2_0', ax, ![C : $t, B : $t, A : $t]: (![f : (A > (B > C))]: ((('const/list/MAP2' C A B) f ('const/list/NIL' A) ('const/list/NIL' B)) = ('const/list/NIL' C)))).
tt('thm/list/MAP2_e1', ax, ![E : $t, D : $t, F : $t]: (![f : (D > (E > F)), h1 : D, t1 : ('type/list/list' D), h2 : E, t2 : ('type/list/list' E)]: ((('const/list/MAP2' F D E) f (('const/list/CONS' D) h1 t1) (('const/list/CONS' E) h2 t2)) = (('const/list/CONS' F) (f h1 h2) (('const/list/MAP2' F D E) f t1 t2))))).
tt('thm/list/INDEX_FIND_def_0', def, ![A : $t]: (![i : 'type/num/num', P : (A > $o)]: ((('const/list/INDEX_FIND' A) i P ('const/list/NIL' A)) = ('const/option/NONE' ('type/pair/prod' 'type/num/num' A))))).
tt('thm/list/INDEX_FIND_def_e1', def, ![A : $t]: (![i : 'type/num/num', P : (A > $o), h : A, t : ('type/list/list' A)]: ((('const/list/INDEX_FIND' A) i P (('const/list/CONS' A) h t)) = (('const/bool/COND' ('type/option/option' ('type/pair/prod' 'type/num/num' A))) (P h) (('const/option/SOME' ('type/pair/prod' 'type/num/num' A)) (('const/pair/,' 'type/num/num' A) i h)) (('const/list/INDEX_FIND' A) ('const/num/SUC' i) P t))))).
tt('thm/list/FIND_def_', def, ![A : $t]: (![P : (A > $o)]: ((('const/list/FIND' A) P) = (('const/combin/o' ('type/list/list' A) ('type/option/option' A) ('type/option/option' ('type/pair/prod' 'type/num/num' A))) (('const/option/OPTION_MAP' ('type/pair/prod' 'type/num/num' A) A) ('const/pair/SND' 'type/num/num' A)) (('const/list/INDEX_FIND' A) 'const/num/0' P))))).
tt('thm/list/INDEX_OF_def_', def, ![A : $t]: (![x : A]: ((('const/list/INDEX_OF' A) x) = (('const/combin/o' ('type/list/list' A) ('type/option/option' 'type/num/num') ('type/option/option' ('type/pair/prod' 'type/num/num' A))) (('const/option/OPTION_MAP' ('type/pair/prod' 'type/num/num' A) 'type/num/num') ('const/pair/FST' 'type/num/num' A)) (('const/list/INDEX_FIND' A) 'const/num/0' (($equals A) x)))))).
tt('thm/list/NULL_0', ax, ![A : $t]: (('const/list/NULL' A) ('const/list/NIL' A))).
tt('thm/list/NULL_e1', ax, ![A : $t]: (![h : A, t : ('type/list/list' A)]: (~ (('const/list/NULL' A) (('const/list/CONS' A) h t))))).
tt('thm/list/list_INDUCT_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: (((P ('const/list/NIL' A)) & (![t : ('type/list/list' A)]: ((P t) => (![h : A]: (P (('const/list/CONS' A) h t)))))) => (![l : ('type/list/list' A)]: (P l))))).
tt('thm/list/list_induction_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: (((P ('const/list/NIL' A)) & (![t : ('type/list/list' A)]: ((P t) => (![h : A]: (P (('const/list/CONS' A) h t)))))) => (![l : ('type/list/list' A)]: (P l))))).
tt('thm/list/list_CASES_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((l = ('const/list/NIL' A)) | (?[h : A, t : ('type/list/list' A)]: (l = (('const/list/CONS' A) h t)))))).
tt('thm/list/list_nchotomy_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((l = ('const/list/NIL' A)) | (?[h : A, t : ('type/list/list' A)]: (l = (('const/list/CONS' A) h t)))))).
tt('thm/list/list_case_compute_', ax, ![A : $t, B : $t]: (![f : (A > (('type/list/list' A) > B)), b : B, l : ('type/list/list' A)]: ((('const/list/list_CASE' A B) l b f) = (('const/bool/COND' B) (('const/list/NULL' A) l) b (f (('const/list/HD' A) l) (('const/list/TL' A) l)))))).
tt('thm/list/CONS_11_', ax, ![A : $t]: (![a0 : A, a1 : ('type/list/list' A), 'a0\'' : A, 'a1\'' : ('type/list/list' A)]: (((('const/list/CONS' A) a0 a1) = (('const/list/CONS' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/list/NOT_NIL_CONS_', ax, ![A : $t]: (![a1 : ('type/list/list' A), a0 : A]: (~ (('const/list/NIL' A) = (('const/list/CONS' A) a0 a1))))).
tt('thm/list/NOT_CONS_NIL_', ax, ![A : $t]: (![a1 : ('type/list/list' A), a0 : A]: (~ ((('const/list/CONS' A) a0 a1) = ('const/list/NIL' A))))).
tt('thm/list/LIST_NOT_EQ_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((~ (l1 = l2)) => (![h1 : A, h2 : A]: (~ ((('const/list/CONS' A) h1 l1) = (('const/list/CONS' A) h2 l2))))))).
tt('thm/list/NOT_EQ_LIST_', ax, ![A : $t]: (![h1 : A, h2 : A]: ((~ (h1 = h2)) => (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (~ ((('const/list/CONS' A) h1 l1) = (('const/list/CONS' A) h2 l2))))))).
tt('thm/list/EQ_LIST_', ax, ![A : $t]: (![h1 : A, h2 : A]: ((h1 = h2) => (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((l1 = l2) => ((('const/list/CONS' A) h1 l1) = (('const/list/CONS' A) h2 l2))))))).
tt('thm/list/CONS_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (('const/list/NULL' A) l)) => ((('const/list/CONS' A) (('const/list/HD' A) l) (('const/list/TL' A) l)) = l)))).
tt('thm/list/APPEND_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/APPEND' A) l ('const/list/NIL' A)) = l))).
tt('thm/list/APPEND_ASSOC_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), l3 : ('type/list/list' A)]: ((('const/list/APPEND' A) l1 (('const/list/APPEND' A) l2 l3)) = (('const/list/APPEND' A) (('const/list/APPEND' A) l1 l2) l3)))).
tt('thm/list/LENGTH_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/APPEND' A) l1 l2)) = ('const/arithmetic/+' (('const/list/LENGTH' A) l1) (('const/list/LENGTH' A) l2))))).
tt('thm/list/MAP_APPEND_', ax, ![A : $t, B : $t]: (![f : (A > B), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/MAP' A B) f (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' B) (('const/list/MAP' A B) f l1) (('const/list/MAP' A B) f l2))))).
tt('thm/list/MAP_ID_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/MAP' A A) (^[x : A]: x) l) = l))).
tt('thm/list/MAP_ID_e1', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/MAP' A A) ('const/combin/I' A) l) = l))).
tt('thm/list/LENGTH_MAP_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), f : (A > B)]: ((('const/list/LENGTH' B) (('const/list/MAP' A B) f l)) = (('const/list/LENGTH' A) l)))).
tt('thm/list/MAP_EQ_NIL_0', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), f : (A > B)]: (((('const/list/MAP' A B) f l) = ('const/list/NIL' B)) = (l = ('const/list/NIL' A))))).
tt('thm/list/MAP_EQ_NIL_e1', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), f : (A > B)]: ((('const/list/NIL' B) = (('const/list/MAP' A B) f l)) = (l = ('const/list/NIL' A))))).
tt('thm/list/MAP_EQ_f_', ax, ![A : $t, B : $t]: (![f1 : (A > B), f2 : (A > B), l : ('type/list/list' A)]: (((('const/list/MAP' A B) f1 l) = (('const/list/MAP' A B) f2 l)) = (![e : A]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)) => ((f1 e) = (f2 e))))))).
tt('thm/list/MAP_o_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), g : (A > B)]: ((('const/list/MAP' A C) (('const/combin/o' A C B) f g)) = (('const/combin/o' ('type/list/list' A) ('type/list/list' C) ('type/list/list' B)) (('const/list/MAP' B C) f) (('const/list/MAP' A B) g))))).
tt('thm/list/MAP_MAP_o_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), g : (A > B), l : ('type/list/list' A)]: ((('const/list/MAP' B C) f (('const/list/MAP' A B) g l)) = (('const/list/MAP' A C) (('const/combin/o' A C B) f g) l)))).
tt('thm/list/EL_MAP_', ax, ![A : $t, B : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (![f : (A > B)]: ((('const/list/EL' B) n (('const/list/MAP' A B) f l)) = (f (('const/list/EL' A) n l))))))).
tt('thm/list/MAP_TL_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), f : (A > B)]: ((~ (('const/list/NULL' A) l)) => ((('const/list/MAP' A B) f (('const/list/TL' A) l)) = (('const/list/TL' B) (('const/list/MAP' A B) f l)))))).
tt('thm/list/EVERY_EL_', ax, ![A : $t]: (![l : ('type/list/list' A), P : (A > $o)]: ((('const/list/EVERY' A) P l) = (![n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (P (('const/list/EL' A) n l))))))).
tt('thm/list/EVERY_CONJ_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) (^[x : A]: ((P x) & (Q x))) l) = ((('const/list/EVERY' A) P l) & (('const/list/EVERY' A) Q l))))).
tt('thm/list/EVERY_MEM_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) = (![e : A]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)) => (P e)))))).
tt('thm/list/EVERY_MAP_', ax, ![A : $t, B : $t]: (![P : (B > $o), f : (A > B), l : ('type/list/list' A)]: ((('const/list/EVERY' B) P (('const/list/MAP' A B) f l)) = (('const/list/EVERY' A) (^[x : A]: (P (f x))) l)))).
tt('thm/list/EVERY_SIMP_', ax, ![A : $t]: (![c : $o, l : ('type/list/list' A)]: ((('const/list/EVERY' A) (^[x : A]: c) l) = ((l = ('const/list/NIL' A)) | c)))).
tt('thm/list/MONO_EVERY_', ax, ![A : $t]: (![l : ('type/list/list' A), Q : (A > $o), P : (A > $o)]: ((![x : A]: ((P x) => (Q x))) => ((('const/list/EVERY' A) P l) => (('const/list/EVERY' A) Q l))))).
tt('thm/list/EXISTS_MEM_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P l) = (?[e : A]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)) & (P e)))))).
tt('thm/list/EXISTS_MAP_', ax, ![A : $t, B : $t]: (![P : (B > $o), f : (A > B), l : ('type/list/list' A)]: ((('const/list/EXISTS' B) P (('const/list/MAP' A B) f l)) = (('const/list/EXISTS' A) (^[x : A]: (P (f x))) l)))).
tt('thm/list/EXISTS_SIMP_', ax, ![A : $t]: (![c : $o, l : ('type/list/list' A)]: ((('const/list/EXISTS' A) (^[x : A]: c) l) = ((~ (l = ('const/list/NIL' A))) & c)))).
tt('thm/list/MONO_EXISTS_', ax, ![A : $t]: (![l : ('type/list/list' A), Q : (A > $o), P : (A > $o)]: ((![x : A]: ((P x) => (Q x))) => ((('const/list/EXISTS' A) P l) => (('const/list/EXISTS' A) Q l))))).
tt('thm/list/EVERY_NOT_EXISTS_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) = (~ (('const/list/EXISTS' A) (^[x : A]: (~ (P x))) l))))).
tt('thm/list/EXISTS_NOT_EVERY_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P l) = (~ (('const/list/EVERY' A) (^[x : A]: (~ (P x))) l))))).
tt('thm/list/MEM_APPEND_', ax, ![A : $t]: (![e : A, l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) (('const/list/APPEND' A) l1 l2))) = ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l1)) | (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l2)))))).
tt('thm/list/MEM_FILTER_', ax, ![A : $t]: (![P : (A > $o), L : ('type/list/list' A), x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/FILTER' A) P L))) = ((P x) & (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) L)))))).
tt('thm/list/MEM_FLAT_', ax, ![A : $t]: (![x : A, L : ('type/list/list' ('type/list/list' A))]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/FLAT' A) L))) = (?[l : ('type/list/list' A)]: ((('const/bool/IN' ('type/list/list' A)) l (('const/list/LIST_TO_SET' ('type/list/list' A)) L)) & (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/list/FLAT_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' ('type/list/list' A)), l2 : ('type/list/list' ('type/list/list' A))]: ((('const/list/FLAT' A) (('const/list/APPEND' ('type/list/list' A)) l1 l2)) = (('const/list/APPEND' A) (('const/list/FLAT' A) l1) (('const/list/FLAT' A) l2))))).
tt('thm/list/EVERY_APPEND_', ax, ![A : $t]: (![P : (A > $o), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/EVERY' A) P (('const/list/APPEND' A) l1 l2)) = ((('const/list/EVERY' A) P l1) & (('const/list/EVERY' A) P l2))))).
tt('thm/list/EXISTS_APPEND_', ax, ![A : $t]: (![P : (A > $o), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/EXISTS' A) P (('const/list/APPEND' A) l1 l2)) = ((('const/list/EXISTS' A) P l1) | (('const/list/EXISTS' A) P l2))))).
tt('thm/list/NOT_EVERY_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((~ (('const/list/EVERY' A) P l)) = (('const/list/EXISTS' A) (('const/combin/o' A $o $o) $not P) l)))).
tt('thm/list/NOT_EXISTS_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((~ (('const/list/EXISTS' A) P l)) = (('const/list/EVERY' A) (('const/combin/o' A $o $o) $not P) l)))).
tt('thm/list/MEM_MAP_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), f : (A > B), x : B]: ((('const/bool/IN' B) x (('const/list/LIST_TO_SET' B) (('const/list/MAP' A B) f l))) = (?[y : A]: ((x = (f y)) & (('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) l))))))).
tt('thm/list/LENGTH_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (((('const/list/LENGTH' A) l) = 'const/num/0') = (l = ('const/list/NIL' A))))).
tt('thm/list/LENGTH_NIL_SYM_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (('const/num/0' = (('const/list/LENGTH' A) l)) = (l = ('const/list/NIL' A))))).
tt('thm/list/NULL_EQ_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/NULL' A) l) = (l = ('const/list/NIL' A))))).
tt('thm/list/NULL_LENGTH_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/NULL' A) l) = ((('const/list/LENGTH' A) l) = 'const/num/0')))).
tt('thm/list/LENGTH_CONS_', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/num/SUC' n)) = (?[h : A, 'l\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) 'l\'') = n) & (l = (('const/list/CONS' A) h 'l\''))))))).
tt('thm/list/LENGTH_EQ_CONS_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o), n : 'type/num/num']: ((![l : ('type/list/list' A)]: (((('const/list/LENGTH' A) l) = ('const/num/SUC' n)) => (P l))) = (![l : ('type/list/list' A)]: (((('const/list/LENGTH' A) l) = n) => ((^[l0 : ('type/list/list' A)]: (![x : A]: (P (('const/list/CONS' A) x l0)))) l)))))).
tt('thm/list/LENGTH_EQ_SUM_', ax, ![A : $t]: (![l : ('type/list/list' A), n1 : 'type/num/num', n2 : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/arithmetic/+' n1 n2)) = (?[l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/LENGTH' A) l1) = n1) & (((('const/list/LENGTH' A) l2) = n2) & (l = (('const/list/APPEND' A) l1 l2)))))))).
tt('thm/list/LENGTH_EQ_NUM_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: (((('const/list/LENGTH' A) l) = 'const/num/0') = (l = ('const/list/NIL' A))))).
tt('thm/list/LENGTH_EQ_NUM_1', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/num/SUC' n)) = (?[h : A, 'l\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) 'l\'') = n) & (l = (('const/list/CONS' A) h 'l\''))))))).
tt('thm/list/LENGTH_EQ_NUM_e2', ax, ![A : $t]: (![l : ('type/list/list' A), n1 : 'type/num/num', n2 : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/arithmetic/+' n1 n2)) = (?[l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/LENGTH' A) l1) = n1) & (((('const/list/LENGTH' A) l2) = n2) & (l = (('const/list/APPEND' A) l1 l2)))))))).
tt('thm/list/LENGTH_EQ_NUM_compute_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: (((('const/list/LENGTH' A) l) = 'const/num/0') = (l = ('const/list/NIL' A))))).
tt('thm/list/LENGTH_EQ_NUM_compute_1', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = (?[h : A, 'l\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) 'l\'') = ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) & (l = (('const/list/CONS' A) h 'l\''))))))).
tt('thm/list/LENGTH_EQ_NUM_compute_2', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = (?[h : A, 'l\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) 'l\'') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) & (l = (('const/list/CONS' A) h 'l\''))))))).
tt('thm/list/LENGTH_EQ_NUM_compute_e3', ax, ![A : $t]: (![l : ('type/list/list' A), n1 : 'type/num/num', n2 : 'type/num/num']: (((('const/list/LENGTH' A) l) = ('const/arithmetic/+' n1 n2)) = (?[l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/LENGTH' A) l1) = n1) & (((('const/list/LENGTH' A) l2) = n2) & (l = (('const/list/APPEND' A) l1 l2)))))))).
tt('thm/list/LENGTH_EQ_NIL_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: ((![l : ('type/list/list' A)]: (((('const/list/LENGTH' A) l) = 'const/num/0') => (P l))) = (P ('const/list/NIL' A))))).
tt('thm/list/CONS_ACYCLIC_0', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: (~ (l = (('const/list/CONS' A) x l))))).
tt('thm/list/CONS_ACYCLIC_e1', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: (~ ((('const/list/CONS' A) x l) = l)))).
tt('thm/list/APPEND_eq_NIL_0', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/NIL' A) = (('const/list/APPEND' A) l1 l2)) = ((l1 = ('const/list/NIL' A)) & (l2 = ('const/list/NIL' A)))))).
tt('thm/list/APPEND_eq_NIL_e1', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/APPEND' A) l1 l2) = ('const/list/NIL' A)) = ((l1 = ('const/list/NIL' A)) & (l2 = ('const/list/NIL' A)))))).
tt('thm/list/APPEND_EQ_SING_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A), e : A]: (((('const/list/APPEND' A) l1 l2) = (('const/list/CONS' A) e ('const/list/NIL' A))) = (((l1 = (('const/list/CONS' A) e ('const/list/NIL' A))) & (l2 = ('const/list/NIL' A))) | ((l1 = ('const/list/NIL' A)) & (l2 = (('const/list/CONS' A) e ('const/list/NIL' A)))))))).
tt('thm/list/APPEND_11_0', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), l3 : ('type/list/list' A)]: (((('const/list/APPEND' A) l1 l2) = (('const/list/APPEND' A) l1 l3)) = (l2 = l3)))).
tt('thm/list/APPEND_11_e1', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), l3 : ('type/list/list' A)]: (((('const/list/APPEND' A) l2 l1) = (('const/list/APPEND' A) l3 l1)) = (l2 = l3)))).
tt('thm/list/APPEND_LENGTH_EQ_', ax, ![A : $t]: (![l1 : ('type/list/list' A), 'l1\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' A) 'l1\'')) => (![l2 : ('type/list/list' A), 'l2\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) l2) = (('const/list/LENGTH' A) 'l2\'')) => (((('const/list/APPEND' A) l1 l2) = (('const/list/APPEND' A) 'l1\'' 'l2\'')) = ((l1 = 'l1\'') & (l2 = 'l2\'')))))))).
tt('thm/list/APPEND_11_LENGTH_0', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), 'l1\'' : ('type/list/list' A), 'l2\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' A) 'l1\'')) => (((('const/list/APPEND' A) l1 l2) = (('const/list/APPEND' A) 'l1\'' 'l2\'')) = ((l1 = 'l1\'') & (l2 = 'l2\'')))))).
tt('thm/list/APPEND_11_LENGTH_e1', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), 'l1\'' : ('type/list/list' A), 'l2\'' : ('type/list/list' A)]: (((('const/list/LENGTH' A) l2) = (('const/list/LENGTH' A) 'l2\'')) => (((('const/list/APPEND' A) l1 l2) = (('const/list/APPEND' A) 'l1\'' 'l2\'')) = ((l1 = 'l1\'') & (l2 = 'l2\'')))))).
tt('thm/list/APPEND_EQ_SELF_0', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/APPEND' A) l1 l2) = l1) = (l2 = ('const/list/NIL' A))))).
tt('thm/list/APPEND_EQ_SELF_1', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/APPEND' A) l1 l2) = l2) = (l1 = ('const/list/NIL' A))))).
tt('thm/list/APPEND_EQ_SELF_2', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((l1 = (('const/list/APPEND' A) l1 l2)) = (l2 = ('const/list/NIL' A))))).
tt('thm/list/APPEND_EQ_SELF_e3', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((l2 = (('const/list/APPEND' A) l1 l2)) = (l1 = ('const/list/NIL' A))))).
tt('thm/list/MEM_SPLIT_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) = (?[l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (l = (('const/list/APPEND' A) l1 (('const/list/CONS' A) x l2))))))).
tt('thm/list/LIST_EQ_REWRITE_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((l1 = l2) = (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' A) l2)) & (![x : 'type/num/num']: (('const/prim_rec/<' x (('const/list/LENGTH' A) l1)) => ((('const/list/EL' A) x l1) = (('const/list/EL' A) x l2)))))))).
tt('thm/list/LIST_EQ_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' A) l2)) & (![x : 'type/num/num']: (('const/prim_rec/<' x (('const/list/LENGTH' A) l1)) => ((('const/list/EL' A) x l1) = (('const/list/EL' A) x l2))))) => (l1 = l2)))).
tt('thm/list/FOLDL_EQ_FOLDR_', ax, ![A : $t]: (![f : (A > (A > A)), l : ('type/list/list' A), e : A]: (((('const/operator/ASSOC' A) f) & (('const/operator/COMM' A A) f)) => ((('const/list/FOLDL' A A) f e l) = (('const/list/FOLDR' A A) f e l))))).
tt('thm/list/FOLDR_CONS_', ax, ![B : $t, A : $t]: (![f : (A > B), ls : ('type/list/list' A), a : ('type/list/list' B)]: ((('const/list/FOLDR' A ('type/list/list' B)) (^[x : A, y : ('type/list/list' B)]: (('const/list/CONS' B) (f x) y)) a ls) = (('const/list/APPEND' B) (('const/list/MAP' A B) f ls) a)))).
tt('thm/list/LENGTH_TL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (('const/prim_rec/<' 'const/num/0' (('const/list/LENGTH' A) l)) => ((('const/list/LENGTH' A) (('const/list/TL' A) l)) = ('const/arithmetic/-' (('const/list/LENGTH' A) l) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/list/FILTER_EQ_NIL_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: (((('const/list/FILTER' A) P l) = ('const/list/NIL' A)) = (('const/list/EVERY' A) (^[x : A]: (~ (P x))) l)))).
tt('thm/list/FILTER_NEQ_NIL_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((~ ((('const/list/FILTER' A) P l) = ('const/list/NIL' A))) = (?[x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) & (P x)))))).
tt('thm/list/FILTER_EQ_ID_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: (((('const/list/FILTER' A) P l) = l) = (('const/list/EVERY' A) P l)))).
tt('thm/list/FILTER_NEQ_ID_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((~ ((('const/list/FILTER' A) P l) = l)) = (?[x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) & (~ (P x))))))).
tt('thm/list/FILTER_EQ_CONS_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A), h : A, lr : ('type/list/list' A)]: (((('const/list/FILTER' A) P l) = (('const/list/CONS' A) h lr)) = (?[l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((l = (('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) h ('const/list/NIL' A))) l2)) & (((('const/list/FILTER' A) P l1) = ('const/list/NIL' A)) & (((('const/list/FILTER' A) P l2) = lr) & (P h)))))))).
tt('thm/list/FILTER_APPEND_DISTRIB_', ax, ![A : $t]: (![P : (A > $o), L : ('type/list/list' A), M : ('type/list/list' A)]: ((('const/list/FILTER' A) P (('const/list/APPEND' A) L M)) = (('const/list/APPEND' A) (('const/list/FILTER' A) P L) (('const/list/FILTER' A) P M))))).
tt('thm/list/MEM_0', ax, ![A : $t]: (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ('const/list/NIL' A))) = $false))).
tt('thm/list/MEM_e1', ax, ![A : $t]: (![x : A, h : A, t : ('type/list/list' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/CONS' A) h t))) = ((x = h) | (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) t)))))).
tt('thm/list/FILTER_EQ_APPEND_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/FILTER' A) P l) = (('const/list/APPEND' A) l1 l2)) = (?[l3 : ('type/list/list' A), l4 : ('type/list/list' A)]: ((l = (('const/list/APPEND' A) l3 l4)) & (((('const/list/FILTER' A) P l3) = l1) & ((('const/list/FILTER' A) P l4) = l2))))))).
tt('thm/list/EVERY_FILTER_', ax, ![A : $t]: (![P1 : (A > $o), P2 : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P1 (('const/list/FILTER' A) P2 l)) = (('const/list/EVERY' A) (^[x : A]: ((P2 x) => (P1 x))) l)))).
tt('thm/list/EVERY_FILTER_IMP_', ax, ![A : $t]: (![P1 : (A > $o), P2 : (A > $o), l : ('type/list/list' A)]: ((('const/list/EVERY' A) P1 l) => (('const/list/EVERY' A) P1 (('const/list/FILTER' A) P2 l))))).
tt('thm/list/FILTER_COND_REWRITE_0', ax, ![A : $t]: (![P : (A > $o)]: ((('const/list/FILTER' A) P ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/FILTER_COND_REWRITE_1', ax, ![A : $t]: (![l : ('type/list/list' A), P : (A > $o), h : A]: ((P h) => ((('const/list/FILTER' A) P (('const/list/CONS' A) h l)) = (('const/list/CONS' A) h (('const/list/FILTER' A) P l)))))).
tt('thm/list/FILTER_COND_REWRITE_e2', ax, ![A : $t]: (![l : ('type/list/list' A), P : (A > $o), h : A]: ((~ (P h)) => ((('const/list/FILTER' A) P (('const/list/CONS' A) h l)) = (('const/list/FILTER' A) P l))))).
tt('thm/list/NOT_NULL_MEM_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (('const/list/NULL' A) l)) = (?[e : A]: (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)))))).
tt('thm/list/EL_compute_', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: ((('const/list/EL' A) n l) = (('const/bool/COND' A) (n = 'const/num/0') (('const/list/HD' A) l) (('const/list/EL' A) ('const/prim_rec/PRE' n) (('const/list/TL' A) l)))))).
tt('thm/list/EL_simp_0', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/EL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) l) = (('const/list/EL' A) ('const/prim_rec/PRE' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) (('const/list/TL' A) l))))).
tt('thm/list/EL_simp_e1', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/EL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) l) = (('const/list/EL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/TL' A) l))))).
tt('thm/list/EL_restricted_0', ax, ![A : $t]: ((('const/list/EL' A) 'const/num/0') = ('const/list/HD' A))).
tt('thm/list/EL_restricted_e1', ax, ![B : $t]: (![n : 'type/num/num', ls : ('type/list/list' B), l : B]: ((('const/list/EL' B) ('const/num/SUC' n) (('const/list/CONS' B) l ls)) = (('const/list/EL' B) n ls)))).
tt('thm/list/EL_simp_restricted_0', ax, ![A : $t]: (![n : 'type/num/num', ls : ('type/list/list' A), l : A]: ((('const/list/EL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/CONS' A) l ls)) = (('const/list/EL' A) ('const/prim_rec/PRE' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) ls)))).
tt('thm/list/EL_simp_restricted_e1', ax, ![A : $t]: (![n : 'type/num/num', ls : ('type/list/list' A), l : A]: ((('const/list/EL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) (('const/list/CONS' A) l ls)) = (('const/list/EL' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ls)))).
tt('thm/list/SUM_eq_0_', ax, (![ls : ('type/list/list' 'type/num/num')]: ((('const/list/SUM' ls) = 'const/num/0') = (![x : 'type/num/num']: ((('const/bool/IN' 'type/num/num') x (('const/list/LIST_TO_SET' 'type/num/num') ls)) => (x = 'const/num/0')))))).
tt('thm/list/NULL_FILTER_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A)]: ((('const/list/NULL' A) (('const/list/FILTER' A) P ls)) = (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ls)) => (~ (P x))))))).
tt('thm/list/WF_LIST_PRED_', ax, ![A : $t]: (('const/relation/WF' ('type/list/list' A)) (^[L1 : ('type/list/list' A), L2 : ('type/list/list' A)]: (?[h : A]: (L2 = (('const/list/CONS' A) h L1)))))).
tt('thm/list/LIST_REL_rules_0', ax, ![B : $t, A : $t]: (![R : (A > (B > $o))]: (('const/list/LIST_REL' A B) R ('const/list/NIL' A) ('const/list/NIL' B)))).
tt('thm/list/LIST_REL_rules_e1', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), h1 : A, h2 : B, t1 : ('type/list/list' A), t2 : ('type/list/list' B)]: (((R h1 h2) & (('const/list/LIST_REL' A B) R t1 t2)) => (('const/list/LIST_REL' A B) R (('const/list/CONS' A) h1 t1) (('const/list/CONS' B) h2 t2))))).
tt('thm/list/LIST_REL_ind_', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), 'LIST_REL\'' : (('type/list/list' A) > (('type/list/list' B) > $o))]: ((('LIST_REL\'' ('const/list/NIL' A) ('const/list/NIL' B)) & (![h1 : A, h2 : B, t1 : ('type/list/list' A), t2 : ('type/list/list' B)]: (((R h1 h2) & ('LIST_REL\'' t1 t2)) => ('LIST_REL\'' (('const/list/CONS' A) h1 t1) (('const/list/CONS' B) h2 t2))))) => (![a0 : ('type/list/list' A), a1 : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) R a0 a1) => ('LIST_REL\'' a0 a1)))))).
tt('thm/list/LIST_REL_strongind_', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), 'LIST_REL\'' : (('type/list/list' A) > (('type/list/list' B) > $o))]: ((('LIST_REL\'' ('const/list/NIL' A) ('const/list/NIL' B)) & (![h1 : A, h2 : B, t1 : ('type/list/list' A), t2 : ('type/list/list' B)]: (((R h1 h2) & ((('const/list/LIST_REL' A B) R t1 t2) & ('LIST_REL\'' t1 t2))) => ('LIST_REL\'' (('const/list/CONS' A) h1 t1) (('const/list/CONS' B) h2 t2))))) => (![a0 : ('type/list/list' A), a1 : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) R a0 a1) => ('LIST_REL\'' a0 a1)))))).
tt('thm/list/LIST_REL_cases_', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), a0 : ('type/list/list' A), a1 : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) R a0 a1) = (((a0 = ('const/list/NIL' A)) & (a1 = ('const/list/NIL' B))) | (?[h1 : A, h2 : B, t1 : ('type/list/list' A), t2 : ('type/list/list' B)]: ((a0 = (('const/list/CONS' A) h1 t1)) & ((a1 = (('const/list/CONS' B) h2 t2)) & ((R h1 h2) & (('const/list/LIST_REL' A B) R t1 t2))))))))).
tt('thm/list/LIST_REL_EL_EQN_', 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 l2) = (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) & (![n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) l1)) => (R (('const/list/EL' A) n l1) (('const/list/EL' B) n l2)))))))).
tt('thm/list/LIST_REL_def_0', ax, ![B : $t, A : $t]: (![R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R ('const/list/NIL' A) ('const/list/NIL' B)) = $true))).
tt('thm/list/LIST_REL_def_1', ax, ![B : $t, A : $t]: (![as : ('type/list/list' A), a : A, R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R (('const/list/CONS' A) a as) ('const/list/NIL' B)) = $false))).
tt('thm/list/LIST_REL_def_2', ax, ![B : $t, A : $t]: (![bs : ('type/list/list' B), b : B, R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R ('const/list/NIL' A) (('const/list/CONS' B) b bs)) = $false))).
tt('thm/list/LIST_REL_def_e3', ax, ![B : $t, A : $t]: (![bs : ('type/list/list' B), b : B, as : ('type/list/list' A), a : A, R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R (('const/list/CONS' A) a as) (('const/list/CONS' B) b bs)) = ((R a b) & (('const/list/LIST_REL' A B) R as bs))))).
tt('thm/list/LIST_REL_mono_', ax, ![B : $t, A : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' A), R2 : (A > (B > $o)), R1 : (A > (B > $o))]: ((![x : A, y : B]: ((R1 x y) => (R2 x y))) => ((('const/list/LIST_REL' A B) R1 l1 l2) => (('const/list/LIST_REL' A B) R2 l1 l2))))).
tt('thm/list/LIST_REL_NIL_0', ax, ![B : $t, A : $t]: (![x : ('type/list/list' B), R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R ('const/list/NIL' A) x) = (x = ('const/list/NIL' B))))).
tt('thm/list/LIST_REL_NIL_e1', ax, ![B : $t, A : $t]: (![y : ('type/list/list' B), R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R ('const/list/NIL' A) y) = (y = ('const/list/NIL' B))))).
tt('thm/list/LIST_REL_CONS1_', ax, ![B : $t, A : $t]: (![xs : ('type/list/list' B), t : ('type/list/list' A), h : A, R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R (('const/list/CONS' A) h t) xs) = (?['h\'' : B, 't\'' : ('type/list/list' B)]: ((xs = (('const/list/CONS' B) 'h\'' 't\'')) & ((R h 'h\'') & (('const/list/LIST_REL' A B) R t 't\''))))))).
tt('thm/list/LIST_REL_CONS2_', ax, ![B : $t, A : $t]: (![xs : ('type/list/list' A), t : ('type/list/list' B), h : B, R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R xs (('const/list/CONS' B) h t)) = (?['h\'' : A, 't\'' : ('type/list/list' A)]: ((xs = (('const/list/CONS' A) 'h\'' 't\'')) & ((R 'h\'' h) & (('const/list/LIST_REL' A B) R 't\'' t))))))).
tt('thm/list/LIST_REL_CONJ_', ax, ![B : $t, A : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' A), Q : (A > (B > $o)), P : (A > (B > $o))]: ((('const/list/LIST_REL' A B) (^[a : A, b : B]: ((P a b) & (Q a b))) l1 l2) = ((('const/list/LIST_REL' A B) (^[a : A, b : B]: (P a b)) l1 l2) & (('const/list/LIST_REL' A B) (^[a : A, b : B]: (Q a b)) l1 l2))))).
tt('thm/list/LIST_REL_MAP1_', ax, ![B : $t, C : $t, A : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' C), f : (C > A), R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) R (('const/list/MAP' C A) f l1) l2) = (('const/list/LIST_REL' C B) (('const/combin/o' C (B > $o) A) R f) l1 l2)))).
tt('thm/list/LIST_REL_MAP2_', ax, ![C : $t, A : $t, B : $t]: (![l2 : ('type/list/list' C), l1 : ('type/list/list' A), f : (C > B), R : (A > (B > $o))]: ((('const/list/LIST_REL' A B) (^[a : A, b : B]: (R a b)) l1 (('const/list/MAP' C B) f l2)) = (('const/list/LIST_REL' A C) (^[a : A, b : C]: (R a (f b))) l1 l2)))).
tt('thm/list/LIST_REL_LENGTH_', ax, ![B : $t, A : $t]: (![R : (A > (B > $o)), x : ('type/list/list' A), y : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) R x y) => ((('const/list/LENGTH' A) x) = (('const/list/LENGTH' B) y))))).
tt('thm/list/list_size_cong_', ax, ![A : $t]: (![M : ('type/list/list' A), N : ('type/list/list' A), f : (A > 'type/num/num'), 'f\'' : (A > 'type/num/num')]: (((M = N) & (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) N)) => ((f x) = ('f\'' x))))) => ((('const/list/list_size' A) f M) = (('const/list/list_size' A) 'f\'' N))))).
tt('thm/list/FOLDR_CONG_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), 'l\'' : ('type/list/list' A), b : B, 'b\'' : B, f : (A > (B > B)), 'f\'' : (A > (B > B))]: (((l = 'l\'') & ((b = 'b\'') & (![x : A, a : B]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) 'l\'')) => ((f x a) = ('f\'' x a)))))) => ((('const/list/FOLDR' A B) f b l) = (('const/list/FOLDR' A B) 'f\'' 'b\'' 'l\''))))).
tt('thm/list/FOLDL_CONG_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' A), 'l\'' : ('type/list/list' A), b : B, 'b\'' : B, f : (B > (A > B)), 'f\'' : (B > (A > B))]: (((l = 'l\'') & ((b = 'b\'') & (![x : A, a : B]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) 'l\'')) => ((f a x) = ('f\'' a x)))))) => ((('const/list/FOLDL' A B) f b l) = (('const/list/FOLDL' A B) 'f\'' 'b\'' 'l\''))))).
tt('thm/list/MAP_CONG_', ax, ![A : $t, B : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), f : (A > B), 'f\'' : (A > B)]: (((l1 = l2) & (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l2)) => ((f x) = ('f\'' x))))) => ((('const/list/MAP' A B) f l1) = (('const/list/MAP' A B) 'f\'' l2))))).
tt('thm/list/MAP2_CONG_', ax, ![B : $t, A : $t, C : $t]: (![l1 : ('type/list/list' A), 'l1\'' : ('type/list/list' A), l2 : ('type/list/list' B), 'l2\'' : ('type/list/list' B), f : (A > (B > C)), 'f\'' : (A > (B > C))]: (((l1 = 'l1\'') & ((l2 = 'l2\'') & (![x : A, y : B]: (((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) 'l1\'')) & (('const/bool/IN' B) y (('const/list/LIST_TO_SET' B) 'l2\''))) => ((f x y) = ('f\'' x y)))))) => ((('const/list/MAP2' C A B) f l1 l2) = (('const/list/MAP2' C A B) 'f\'' 'l1\'' 'l2\''))))).
tt('thm/list/EXISTS_CONG_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), P : (A > $o), 'P\'' : (A > $o)]: (((l1 = l2) & (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l2)) => ((P x) = ('P\'' x))))) => ((('const/list/EXISTS' A) P l1) = (('const/list/EXISTS' A) 'P\'' l2))))).
tt('thm/list/EVERY_CONG_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), P : (A > $o), 'P\'' : (A > $o)]: (((l1 = l2) & (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l2)) => ((P x) = ('P\'' x))))) => ((('const/list/EVERY' A) P l1) = (('const/list/EVERY' A) 'P\'' l2))))).
tt('thm/list/EVERY_MONOTONIC_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o)]: ((![x : A]: ((P x) => (Q x))) => (![l : ('type/list/list' A)]: ((('const/list/EVERY' A) P l) => (('const/list/EVERY' A) Q l)))))).
tt('thm/list/ZIP_0', def, ![A : $t, B : $t]: ((('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) ('const/list/NIL' A) ('const/list/NIL' B))) = ('const/list/NIL' ('type/pair/prod' A B)))).
tt('thm/list/ZIP_e1', def, ![B : $t, A : $t]: (![x1 : A, l1 : ('type/list/list' A), x2 : B, l2 : ('type/list/list' B)]: ((('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/CONS' A) x1 l1) (('const/list/CONS' B) x2 l2))) = (('const/list/CONS' ('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/list/UNZIP_0', def, ![B : $t, A : $t]: ((('const/list/UNZIP' A B) ('const/list/NIL' ('type/pair/prod' A B))) = (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) ('const/list/NIL' A) ('const/list/NIL' B)))).
tt('thm/list/UNZIP_e1', def, ![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/CONS' ('type/pair/prod' A B)) x l)) = (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/CONS' 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/CONS' 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/list/UNZIP_THM_0', ax, ![B : $t, A : $t]: ((('const/list/UNZIP' A B) ('const/list/NIL' ('type/pair/prod' A B))) = (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) ('const/list/NIL' A) ('const/list/NIL' B)))).
tt('thm/list/UNZIP_THM_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, t : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/UNZIP' A B) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) t)) = (('const/bool/LET' ('type/pair/prod' ('type/list/list' A) ('type/list/list' B)) ('type/pair/prod' ('type/list/list' A) ('type/list/list' B))) (('const/pair/UNCURRY' ('type/list/list' A) ('type/list/list' B) ('type/pair/prod' ('type/list/list' A) ('type/list/list' B))) (^[L1 : ('type/list/list' A), L2 : ('type/list/list' B)]: (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/CONS' A) x L1) (('const/list/CONS' B) y L2)))) (('const/list/UNZIP' A B) t))))).
tt('thm/list/UNZIP_MAP_', ax, ![A : $t, B : $t]: (![L : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/UNZIP' A B) L) = (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) L) (('const/list/MAP' ('type/pair/prod' A B) B) ('const/pair/SND' A B) L))))).
tt('thm/list/LENGTH_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/LENGTH' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/LENGTH' A) l1)) & ((('const/list/LENGTH' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/LENGTH' B) l2)))))).
tt('thm/list/LENGTH_UNZIP_0', ax, ![A : $t, B : $t]: (![pl : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/LENGTH' A) (('const/pair/FST' ('type/list/list' A) ('type/list/list' B)) (('const/list/UNZIP' A B) pl))) = (('const/list/LENGTH' ('type/pair/prod' A B)) pl)))).
tt('thm/list/LENGTH_UNZIP_e1', ax, ![A : $t, B : $t]: (![pl : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/LENGTH' B) (('const/pair/SND' ('type/list/list' A) ('type/list/list' B)) (('const/list/UNZIP' A B) pl))) = (('const/list/LENGTH' ('type/pair/prod' A B)) pl)))).
tt('thm/list/ZIP_UNZIP_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/ZIP' A B) (('const/list/UNZIP' A B) l)) = l))).
tt('thm/list/UNZIP_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/UNZIP' A B) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))))).
tt('thm/list/ZIP_MAP_', ax, ![B : $t, A : $t, D : $t, C : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B), f1 : (A > C), f2 : (B > D)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => (((('const/list/ZIP' C B) (('const/pair/,' ('type/list/list' C) ('type/list/list' B)) (('const/list/MAP' A C) f1 l1) l2)) = (('const/list/MAP' ('type/pair/prod' A B) ('type/pair/prod' C B)) (^[p : ('type/pair/prod' A B)]: (('const/pair/,' C B) (f1 (('const/pair/FST' A B) p)) (('const/pair/SND' A B) p))) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))) & ((('const/list/ZIP' A D) (('const/pair/,' ('type/list/list' A) ('type/list/list' D)) l1 (('const/list/MAP' B D) f2 l2))) = (('const/list/MAP' ('type/pair/prod' A B) ('type/pair/prod' A D)) (^[p : ('type/pair/prod' A B)]: (('const/pair/,' A D) (('const/pair/FST' A B) p) (f2 (('const/pair/SND' A B) p)))) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))))))).
tt('thm/list/MEM_ZIP_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B), p : ('type/pair/prod' A B)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => ((('const/bool/IN' ('type/pair/prod' A B)) p (('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)) l1 l2)))) = (?[n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) l1)) & (p = (('const/pair/,' A B) (('const/list/EL' A) n l1) (('const/list/EL' B) n l2))))))))).
tt('thm/list/EL_ZIP_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B), n : 'type/num/num']: ((((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) & ('const/prim_rec/<' n (('const/list/LENGTH' A) l1))) => ((('const/list/EL' ('type/pair/prod' A B)) n (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/pair/,' A B) (('const/list/EL' A) n l1) (('const/list/EL' B) n l2)))))).
tt('thm/list/MAP2_ZIP_', 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/MAP2' C A B) f l1 l2) = (('const/list/MAP' ('type/pair/prod' A B) C) (('const/pair/UNCURRY' A B C) f) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))))))).
tt('thm/list/MAP2_MAP_', 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/MAP2' C A B) f l1 l2) = (('const/list/MAP' ('type/pair/prod' A B) C) (('const/pair/UNCURRY' A B C) f) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))))))).
tt('thm/list/MAP_ZIP_', ax, ![B : $t, D : $t, A : $t, C : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' A), g : (B > D), f : (A > C)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => (((('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = l1) & (((('const/list/MAP' ('type/pair/prod' A B) B) ('const/pair/SND' A B) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = l2) & (((('const/list/MAP' ('type/pair/prod' A B) C) (('const/combin/o' ('type/pair/prod' A B) C A) f ('const/pair/FST' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/MAP' A C) f l1)) & ((('const/list/MAP' ('type/pair/prod' A B) D) (('const/combin/o' ('type/pair/prod' A B) D B) g ('const/pair/SND' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/MAP' B D) g l2)))))))).
tt('thm/list/MEM_EL_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) = (?[n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) & (x = (('const/list/EL' A) n l))))))).
tt('thm/list/SUM_MAP_PLUS_ZIP_', ax, ![B : $t, A : $t]: (![h : (B > 'type/num/num'), g : (A > 'type/num/num'), f : (('type/pair/prod' A B) > 'type/num/num'), ls1 : ('type/list/list' A), ls2 : ('type/list/list' B)]: ((((('const/list/LENGTH' A) ls1) = (('const/list/LENGTH' B) ls2)) & (![x : A, y : B]: ((f (('const/pair/,' A B) x y)) = ('const/arithmetic/+' (g x) (h y))))) => (('const/list/SUM' (('const/list/MAP' ('type/pair/prod' A B) 'type/num/num') f (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) ls1 ls2)))) = ('const/arithmetic/+' ('const/list/SUM' (('const/list/MAP' A 'type/num/num') g ls1)) ('const/list/SUM' (('const/list/MAP' B 'type/num/num') h ls2))))))).
tt('thm/list/LIST_REL_EVERY_ZIP_', 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 l2) = (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) & (('const/list/EVERY' ('type/pair/prod' A B)) (('const/pair/UNCURRY' A B $o) R) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))))))).
tt('thm/list/REVERSE_DEF_0', def, ![A : $t]: ((('const/list/REVERSE' A) ('const/list/NIL' A)) = ('const/list/NIL' A))).
tt('thm/list/REVERSE_DEF_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/REVERSE' A) (('const/list/CONS' A) h t)) = (('const/list/APPEND' A) (('const/list/REVERSE' A) t) (('const/list/CONS' A) h ('const/list/NIL' A)))))).
tt('thm/list/REVERSE_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/REVERSE' A) (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/list/REVERSE' A) l2) (('const/list/REVERSE' A) l1))))).
tt('thm/list/REVERSE_REVERSE_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/REVERSE' A) (('const/list/REVERSE' A) l)) = l))).
tt('thm/list/REVERSE_11_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/REVERSE' A) l1) = (('const/list/REVERSE' A) l2)) = (l1 = l2)))).
tt('thm/list/MEM_REVERSE_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/REVERSE' A) l))) = (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))))).
tt('thm/list/LENGTH_REVERSE_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/REVERSE' A) l)) = (('const/list/LENGTH' A) l)))).
tt('thm/list/REVERSE_EQ_NIL_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (((('const/list/REVERSE' A) l) = ('const/list/NIL' A)) = (l = ('const/list/NIL' A))))).
tt('thm/list/REVERSE_EQ_SING_', ax, ![A : $t]: (![l : ('type/list/list' A), e : A]: (((('const/list/REVERSE' A) l) = (('const/list/CONS' A) e ('const/list/NIL' A))) = (l = (('const/list/CONS' A) e ('const/list/NIL' A)))))).
tt('thm/list/FILTER_REVERSE_', ax, ![A : $t]: (![l : ('type/list/list' A), P : (A > $o)]: ((('const/list/FILTER' A) P (('const/list/REVERSE' A) l)) = (('const/list/REVERSE' A) (('const/list/FILTER' A) P l))))).
tt('thm/list/LAST_DEF_', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/LAST' A) (('const/list/CONS' A) h t)) = (('const/bool/COND' A) (t = ('const/list/NIL' A)) h (('const/list/LAST' A) t))))).
tt('thm/list/FRONT_DEF_', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/FRONT' A) (('const/list/CONS' A) h t)) = (('const/bool/COND' ('type/list/list' A)) (t = ('const/list/NIL' A)) ('const/list/NIL' A) (('const/list/CONS' A) h (('const/list/FRONT' A) t)))))).
tt('thm/list/LAST_CONS_0', ax, ![A : $t]: (![x : A]: ((('const/list/LAST' A) (('const/list/CONS' A) x ('const/list/NIL' A))) = x))).
tt('thm/list/LAST_CONS_e1', ax, ![A : $t]: (![x : A, y : A, z : ('type/list/list' A)]: ((('const/list/LAST' A) (('const/list/CONS' A) x (('const/list/CONS' A) y z))) = (('const/list/LAST' A) (('const/list/CONS' A) y z))))).
tt('thm/list/LAST_EL_', ax, ![A : $t]: (![ls : ('type/list/list' A)]: ((~ (ls = ('const/list/NIL' A))) => ((('const/list/LAST' A) ls) = (('const/list/EL' A) ('const/prim_rec/PRE' (('const/list/LENGTH' A) ls)) ls))))).
tt('thm/list/FRONT_CONS_0', ax, ![A : $t]: (![x : A]: ((('const/list/FRONT' A) (('const/list/CONS' A) x ('const/list/NIL' A))) = ('const/list/NIL' A)))).
tt('thm/list/FRONT_CONS_e1', ax, ![A : $t]: (![x : A, y : A, z : ('type/list/list' A)]: ((('const/list/FRONT' A) (('const/list/CONS' A) x (('const/list/CONS' A) y z))) = (('const/list/CONS' A) x (('const/list/FRONT' A) (('const/list/CONS' A) y z)))))).
tt('thm/list/LENGTH_FRONT_CONS_', ax, ![A : $t]: (![x : A, xs : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/FRONT' A) (('const/list/CONS' A) x xs))) = (('const/list/LENGTH' A) xs)))).
tt('thm/list/FRONT_CONS_EQ_NIL_0', ax, ![A : $t]: (![x : A, xs : ('type/list/list' A)]: (((('const/list/FRONT' A) (('const/list/CONS' A) x xs)) = ('const/list/NIL' A)) = (xs = ('const/list/NIL' A))))).
tt('thm/list/FRONT_CONS_EQ_NIL_1', ax, ![A : $t]: (![x : A, xs : ('type/list/list' A)]: ((('const/list/NIL' A) = (('const/list/FRONT' A) (('const/list/CONS' A) x xs))) = (xs = ('const/list/NIL' A))))).
tt('thm/list/FRONT_CONS_EQ_NIL_e2', ax, ![A : $t]: (![x : A, xs : ('type/list/list' A)]: ((('const/list/NULL' A) (('const/list/FRONT' A) (('const/list/CONS' A) x xs))) = (('const/list/NULL' A) xs)))).
tt('thm/list/APPEND_FRONT_LAST_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((~ (l = ('const/list/NIL' A))) => ((('const/list/APPEND' A) (('const/list/FRONT' A) l) (('const/list/CONS' A) (('const/list/LAST' A) l) ('const/list/NIL' A))) = l)))).
tt('thm/list/LAST_CONS_cond_', ax, ![A : $t]: (![t : ('type/list/list' A), h : A]: ((('const/list/LAST' A) (('const/list/CONS' A) h t)) = (('const/bool/COND' A) (t = ('const/list/NIL' A)) h (('const/list/LAST' A) t))))).
tt('thm/list/LAST_APPEND_CONS_', ax, ![A : $t]: (![h : A, l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/LAST' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) h l2))) = (('const/list/LAST' A) (('const/list/CONS' A) h l2))))).
tt('thm/list/TAKE_def_0', def, ![A : $t]: (![n : 'type/num/num']: ((('const/list/TAKE' A) n ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/TAKE_def_e1', def, ![A : $t]: (![n : 'type/num/num', x : A, xs : ('type/list/list' A)]: ((('const/list/TAKE' A) n (('const/list/CONS' A) x xs)) = (('const/bool/COND' ('type/list/list' A)) (n = 'const/num/0') ('const/list/NIL' A) (('const/list/CONS' A) x (('const/list/TAKE' A) ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) xs)))))).
tt('thm/list/DROP_def_0', def, ![A : $t]: (![n : 'type/num/num']: ((('const/list/DROP' A) n ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/DROP_def_e1', def, ![A : $t]: (![n : 'type/num/num', x : A, xs : ('type/list/list' A)]: ((('const/list/DROP' A) n (('const/list/CONS' A) x xs)) = (('const/bool/COND' ('type/list/list' A)) (n = 'const/num/0') (('const/list/CONS' A) x xs) (('const/list/DROP' A) ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) xs))))).
tt('thm/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/list/TAKE_LENGTH_ID_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/TAKE' A) (('const/list/LENGTH' A) l) l) = l))).
tt('thm/list/LENGTH_TAKE_', 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/list/TAKE' A) n l)) = n)))).
tt('thm/list/TAKE_APPEND1_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' n (('const/list/LENGTH' A) l1)) => ((('const/list/TAKE' A) n (('const/list/APPEND' A) l1 l2)) = (('const/list/TAKE' A) n l1))))).
tt('thm/list/TAKE_APPEND2_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A), n : 'type/num/num']: (('const/prim_rec/<' (('const/list/LENGTH' A) l1) n) => ((('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/list/DROP_0_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/DROP' A) 'const/num/0' l) = l))).
tt('thm/list/TAKE_DROP_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/APPEND' A) (('const/list/TAKE' A) n l) (('const/list/DROP' A) n l)) = l))).
tt('thm/list/LENGTH_DROP_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/DROP' A) n l)) = ('const/arithmetic/-' (('const/list/LENGTH' A) l) n)))).
tt('thm/list/MEM_DROP_', ax, ![A : $t]: (![x : A, ls : ('type/list/list' A), n : 'type/num/num']: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/DROP' A) n ls))) = ((('const/prim_rec/<' n (('const/list/LENGTH' A) ls)) & (x = (('const/list/EL' A) n ls))) | (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/DROP' A) ('const/num/SUC' n) ls))))))).
tt('thm/list/DROP_NIL_', ax, ![A : $t]: (![ls : ('type/list/list' A), n : 'type/num/num']: (((('const/list/DROP' A) n ls) = ('const/list/NIL' A)) = ('const/arithmetic/>=' n (('const/list/LENGTH' A) ls))))).
tt('thm/list/FOLDL2_ind_', ax, ![C : $t, B : $t, A : $t]: (![P : ((A > (B > (C > A))) > (A > (('type/list/list' B) > (('type/list/list' C) > $o))))]: (((![f : (A > (B > (C > A))), a : A, b : B, bs : ('type/list/list' B), c : C, cs : ('type/list/list' C)]: ((P f (f a b c) bs cs) => (P f a (('const/list/CONS' B) b bs) (('const/list/CONS' C) c cs)))) & ((![f : (A > (B > (C > A))), a : A, cs : ('type/list/list' C)]: (P f a ('const/list/NIL' B) cs)) & (![f : (A > (B > (C > A))), a : A, v6 : B, v7 : ('type/list/list' B)]: (P f a (('const/list/CONS' B) v6 v7) ('const/list/NIL' C))))) => (![v : (A > (B > (C > A))), v1 : A, v2 : ('type/list/list' B), v3 : ('type/list/list' C)]: (P v v1 v2 v3))))).
tt('thm/list/FOLDL2_def_0', ax, ![C : $t, B : $t, A : $t]: (![f : (A > (B > (C > A))), cs : ('type/list/list' C), c : C, bs : ('type/list/list' B), b : B, a : A]: ((('const/list/FOLDL2' A B C) f a (('const/list/CONS' B) b bs) (('const/list/CONS' C) c cs)) = (('const/list/FOLDL2' A B C) f (f a b c) bs cs)))).
tt('thm/list/FOLDL2_def_1', ax, ![A : $t, C : $t, B : $t]: (![f : (A > (B > (C > A))), cs : ('type/list/list' C), a : A]: ((('const/list/FOLDL2' A B C) f a ('const/list/NIL' B) cs) = a))).
tt('thm/list/FOLDL2_def_e2', ax, ![A : $t, C : $t, B : $t]: (![v7 : ('type/list/list' B), v6 : B, f : (A > (B > (C > A))), a : A]: ((('const/list/FOLDL2' A B C) f a (('const/list/CONS' B) v6 v7) ('const/list/NIL' C)) = a))).
tt('thm/list/FOLDL2_cong_', ax, ![B : $t, A : $t, C : $t]: (![l1 : ('type/list/list' A), 'l1\'' : ('type/list/list' A), l2 : ('type/list/list' B), 'l2\'' : ('type/list/list' B), a : C, 'a\'' : C, f : (C > (A > (B > C))), 'f\'' : (C > (A > (B > C)))]: (((l1 = 'l1\'') & ((l2 = 'l2\'') & ((a = 'a\'') & (![z : C, b : A, c : B]: (((('const/bool/IN' A) b (('const/list/LIST_TO_SET' A) 'l1\'')) & (('const/bool/IN' B) c (('const/list/LIST_TO_SET' B) 'l2\''))) => ((f z b c) = ('f\'' z b c))))))) => ((('const/list/FOLDL2' C A B) f a l1 l2) = (('const/list/FOLDL2' C A B) 'f\'' 'a\'' 'l1\'' 'l2\''))))).
tt('thm/list/FOLDL2_FOLDL_', 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 : (C > (A > (B > C))), a : C]: ((('const/list/FOLDL2' C A B) f a l1 l2) = (('const/list/FOLDL' ('type/pair/prod' A B) C) (^[a0 : C]: (('const/pair/UNCURRY' A B C) (f a0))) a (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))))))).
tt('thm/list/EVERY2_cong_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), 'l1\'' : ('type/list/list' A), l2 : ('type/list/list' B), 'l2\'' : ('type/list/list' B), P : (A > (B > $o)), 'P\'' : (A > (B > $o))]: (((l1 = 'l1\'') & ((l2 = 'l2\'') & (![x : A, y : B]: (((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) 'l1\'')) & (('const/bool/IN' B) y (('const/list/LIST_TO_SET' B) 'l2\''))) => ((P x y) = ('P\'' x y)))))) => ((('const/list/LIST_REL' A B) P l1 l2) = (('const/list/LIST_REL' A B) 'P\'' 'l1\'' 'l2\''))))).
tt('thm/list/MAP_EQ_EVERY2_', ax, ![C : $t, A : $t, B : $t]: (![f1 : (A > B), f2 : (C > B), l1 : ('type/list/list' A), l2 : ('type/list/list' C)]: (((('const/list/MAP' A B) f1 l1) = (('const/list/MAP' C B) f2 l2)) = (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' C) l2)) & (('const/list/LIST_REL' A C) (^[x : A, y : C]: ((f1 x) = (f2 y))) l1 l2))))).
tt('thm/list/EVERY2_EVERY_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B), f : (A > (B > $o))]: ((('const/list/LIST_REL' A B) f l1 l2) = (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) & (('const/list/EVERY' ('type/pair/prod' A B)) (('const/pair/UNCURRY' A B $o) f) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))))))).
tt('thm/list/EVERY2_LENGTH_', ax, ![B : $t, A : $t]: (![P : (A > (B > $o)), l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) P l1 l2) => ((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2))))).
tt('thm/list/EVERY2_mono_', ax, ![B : $t, A : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' A), R2 : (A > (B > $o)), R1 : (A > (B > $o))]: ((![x : A, y : B]: ((R1 x y) => (R2 x y))) => ((('const/list/LIST_REL' A B) R1 l1 l2) => (('const/list/LIST_REL' A B) R2 l1 l2))))).
tt('thm/list/ALL_DISTINCT_0', def, ![A : $t]: ((('const/list/ALL_DISTINCT' A) ('const/list/NIL' A)) = $true)).
tt('thm/list/ALL_DISTINCT_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) (('const/list/CONS' A) h t)) = ((~ (('const/bool/IN' A) h (('const/list/LIST_TO_SET' A) t))) & (('const/list/ALL_DISTINCT' A) t))))).
tt('thm/list/ALL_DISTINCT_FILTER_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) l) = (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) => ((('const/list/FILTER' A) (($equals A) x) l) = (('const/list/CONS' A) x ('const/list/NIL' A)))))))).
tt('thm/list/FILTER_ALL_DISTINCT_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) l) => (('const/list/ALL_DISTINCT' A) (('const/list/FILTER' A) P l))))).
tt('thm/list/ALL_DISTINCT_MAP_', ax, ![A : $t, B : $t]: (![f : (A > B), ls : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' B) (('const/list/MAP' A B) f ls)) => (('const/list/ALL_DISTINCT' A) ls)))).
tt('thm/list/EL_ALL_DISTINCT_EL_EQ_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) l) = (![n1 : 'type/num/num', n2 : 'type/num/num']: ((('const/prim_rec/<' n1 (('const/list/LENGTH' A) l)) & ('const/prim_rec/<' n2 (('const/list/LENGTH' A) l))) => (((('const/list/EL' A) n1 l) = (('const/list/EL' A) n2 l)) = (n1 = n2))))))).
tt('thm/list/ALL_DISTINCT_EL_IMP_', ax, ![A : $t]: (![l : ('type/list/list' A), n1 : 'type/num/num', n2 : 'type/num/num']: (((('const/list/ALL_DISTINCT' A) l) & (('const/prim_rec/<' n1 (('const/list/LENGTH' A) l)) & ('const/prim_rec/<' n2 (('const/list/LENGTH' A) l)))) => (((('const/list/EL' A) n1 l) = (('const/list/EL' A) n2 l)) = (n1 = n2))))).
tt('thm/list/ALL_DISTINCT_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) (('const/list/APPEND' A) l1 l2)) = ((('const/list/ALL_DISTINCT' A) l1) & ((('const/list/ALL_DISTINCT' A) l2) & (![e : A]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l1)) => (~ (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l2)))))))))).
tt('thm/list/ALL_DISTINCT_SING_', ax, ![A : $t]: (![x : A]: (('const/list/ALL_DISTINCT' A) (('const/list/CONS' A) x ('const/list/NIL' A))))).
tt('thm/list/ALL_DISTINCT_ZIP_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: (((('const/list/ALL_DISTINCT' A) l1) & ((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2))) => (('const/list/ALL_DISTINCT' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2)))))).
tt('thm/list/ALL_DISTINCT_ZIP_SWAP_', ax, ![A : $t, B : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: (((('const/list/ALL_DISTINCT' ('type/pair/prod' A B)) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) & ((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2))) => (('const/list/ALL_DISTINCT' ('type/pair/prod' B A)) (('const/list/ZIP' B A) (('const/pair/,' ('type/list/list' B) ('type/list/list' A)) l2 l1)))))).
tt('thm/list/ALL_DISTINCT_REVERSE_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) (('const/list/REVERSE' A) l)) = (('const/list/ALL_DISTINCT' A) l)))).
tt('thm/list/LRC_def_0', def, ![A : $t]: (![R : (A > (A > $o)), x : A, y : A]: ((('const/list/LRC' A) R ('const/list/NIL' A) x y) = (x = y)))).
tt('thm/list/LRC_def_e1', def, ![A : $t]: (![R : (A > (A > $o)), h : A, t : ('type/list/list' A), x : A, y : A]: ((('const/list/LRC' A) R (('const/list/CONS' A) h t) x y) = ((x = h) & (?[z : A]: ((R x z) & (('const/list/LRC' A) R t z y))))))).
tt('thm/list/NRC_LRC_', ax, ![A : $t]: (![y : A, x : A, n : 'type/num/num', R : (A > (A > $o))]: ((('const/arithmetic/NRC' A) R n x y) = (?[ls : ('type/list/list' A)]: ((('const/list/LRC' A) R ls x y) & ((('const/list/LENGTH' A) ls) = n)))))).
tt('thm/list/LRC_MEM_', ax, ![A : $t]: (![y : A, x : A, ls : ('type/list/list' A), e : A, R : (A > (A > $o))]: (((('const/list/LRC' A) R ls x y) & (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) ls))) => (?[z : A, t : ('type/list/list' A)]: ((R e z) & (('const/list/LRC' A) R t z y)))))).
tt('thm/list/LRC_MEM_right_', ax, ![A : $t]: (![y : A, x : A, t : ('type/list/list' A), h : A, e : A, R : (A > (A > $o))]: (((('const/list/LRC' A) R (('const/list/CONS' A) h t) x y) & (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) t))) => (?[z : A, p : ('type/list/list' A)]: ((R z e) & (('const/list/LRC' A) R p x z)))))).
tt('thm/list/LIST_TO_SET_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/LIST_TO_SET' A) (('const/list/APPEND' A) l1 l2)) = (('const/pred_set/UNION' A) (('const/list/LIST_TO_SET' A) l1) (('const/list/LIST_TO_SET' A) l2))))).
tt('thm/list/UNION_APPEND_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/pred_set/UNION' A) (('const/list/LIST_TO_SET' A) l1) (('const/list/LIST_TO_SET' A) l2)) = (('const/list/LIST_TO_SET' A) (('const/list/APPEND' A) l1 l2))))).
tt('thm/list/LIST_TO_SET_EQ_EMPTY_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: (((('const/list/LIST_TO_SET' A) l) = ('const/pred_set/EMPTY' A)) = (l = ('const/list/NIL' A))))).
tt('thm/list/LIST_TO_SET_EQ_EMPTY_e1', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/pred_set/EMPTY' A) = (('const/list/LIST_TO_SET' A) l)) = (l = ('const/list/NIL' A))))).
tt('thm/list/FINITE_LIST_TO_SET_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (('const/pred_set/FINITE' A) (('const/list/LIST_TO_SET' A) l)))).
tt('thm/list/SUM_IMAGE_LIST_TO_SET_upper_bound_', ax, ![A : $t]: (![f : (A > 'type/num/num'), ls : ('type/list/list' A)]: ('const/arithmetic/<=' (('const/pred_set/SUM_IMAGE' A) f (('const/list/LIST_TO_SET' A) ls)) ('const/list/SUM' (('const/list/MAP' A 'type/num/num') f ls))))).
tt('thm/list/SUM_MAP_MEM_bound_', ax, ![A : $t]: (![f : (A > 'type/num/num'), x : A, ls : ('type/list/list' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ls)) => ('const/arithmetic/<=' (f x) ('const/list/SUM' (('const/list/MAP' A 'type/num/num') f ls)))))).
tt('thm/list/INJ_MAP_EQ_', ax, ![A : $t, B : $t]: (![f : (A > B), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/pred_set/INJ' A B) f (('const/pred_set/UNION' A) (('const/list/LIST_TO_SET' A) l1) (('const/list/LIST_TO_SET' A) l2)) ('const/pred_set/UNIV' B)) & ((('const/list/MAP' A B) f l1) = (('const/list/MAP' A B) f l2))) => (l1 = l2)))).
tt('thm/list/CARD_LIST_TO_SET_', ax, ![A : $t]: (![ls : ('type/list/list' A)]: ('const/arithmetic/<=' (('const/pred_set/CARD' A) (('const/list/LIST_TO_SET' A) ls)) (('const/list/LENGTH' A) ls)))).
tt('thm/list/ALL_DISTINCT_CARD_LIST_TO_SET_', ax, ![A : $t]: (![ls : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) ls) => ((('const/pred_set/CARD' A) (('const/list/LIST_TO_SET' A) ls)) = (('const/list/LENGTH' A) ls))))).
tt('thm/list/LIST_TO_SET_REVERSE_', ax, ![A : $t]: (![ls : ('type/list/list' A)]: ((('const/list/LIST_TO_SET' A) (('const/list/REVERSE' A) ls)) = (('const/list/LIST_TO_SET' A) ls)))).
tt('thm/list/LIST_TO_SET_THM_0', ax, ![A : $t]: ((('const/list/LIST_TO_SET' A) ('const/list/NIL' A)) = ('const/pred_set/EMPTY' A))).
tt('thm/list/LIST_TO_SET_THM_e1', ax, ![B : $t]: (![t : ('type/list/list' B), h : B]: ((('const/list/LIST_TO_SET' B) (('const/list/CONS' B) h t)) = (('const/pred_set/INSERT' B) h (('const/list/LIST_TO_SET' B) t))))).
tt('thm/list/LIST_TO_SET_MAP_', ax, ![A : $t, B : $t]: (![f : (A > B), l : ('type/list/list' A)]: ((('const/list/LIST_TO_SET' B) (('const/list/MAP' A B) f l)) = (('const/pred_set/IMAGE' A B) f (('const/list/LIST_TO_SET' A) l))))).
tt('thm/list/LIST_TO_SET_FILTER_', ax, ![A : $t]: (![l : ('type/list/list' A), P : (A > $o)]: ((('const/list/LIST_TO_SET' A) (('const/list/FILTER' A) P l)) = (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (P x)))) (('const/list/LIST_TO_SET' A) l))))).
tt('thm/list/SET_TO_LIST_primitive_', def, ![A : $t]: (('const/list/SET_TO_LIST' A) = (('const/relation/WFREC' (A > $o) ('type/list/list' A)) (('const/min/@' ((A > $o) > ((A > $o) > $o))) (^[R : ((A > $o) > ((A > $o) > $o))]: ((('const/relation/WF' (A > $o)) R) & (![s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (~ (s = ('const/pred_set/EMPTY' A)))) => (R (('const/pred_set/REST' A) s) s)))))) (^[SET_TO_LIST : ((A > $o) > ('type/list/list' A)), s : (A > $o)]: (('const/combin/I' ('type/list/list' A)) (('const/bool/COND' ('type/list/list' A)) (('const/pred_set/FINITE' A) s) (('const/bool/COND' ('type/list/list' A)) (s = ('const/pred_set/EMPTY' A)) ('const/list/NIL' A) (('const/list/CONS' A) (('const/pred_set/CHOICE' A) s) (SET_TO_LIST (('const/pred_set/REST' A) s)))) ('const/bool/ARB' ('type/list/list' A)))))))).
tt('thm/list/SET_TO_LIST_THM_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/list/SET_TO_LIST' A) s) = (('const/bool/COND' ('type/list/list' A)) (s = ('const/pred_set/EMPTY' A)) ('const/list/NIL' A) (('const/list/CONS' A) (('const/pred_set/CHOICE' A) s) (('const/list/SET_TO_LIST' A) (('const/pred_set/REST' A) s)))))))).
tt('thm/list/SET_TO_LIST_IND_', ax, ![A : $t]: (![P : ((A > $o) > $o)]: ((![s : (A > $o)]: ((((('const/pred_set/FINITE' A) s) & (~ (s = ('const/pred_set/EMPTY' A)))) => (P (('const/pred_set/REST' A) s))) => (P s))) => (![v : (A > $o)]: (P v))))).
tt('thm/list/SET_TO_LIST_EMPTY_', ax, ![A : $t]: ((('const/list/SET_TO_LIST' A) ('const/pred_set/EMPTY' A)) = ('const/list/NIL' A))).
tt('thm/list/SET_TO_LIST_INV_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/list/LIST_TO_SET' A) (('const/list/SET_TO_LIST' A) s)) = s)))).
tt('thm/list/SET_TO_LIST_CARD_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/list/LENGTH' A) (('const/list/SET_TO_LIST' A) s)) = (('const/pred_set/CARD' A) s))))).
tt('thm/list/SET_TO_LIST_IN_MEM_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![x : A]: ((('const/bool/IN' A) x s) = (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/SET_TO_LIST' A) s)))))))).
tt('thm/list/MEM_SET_TO_LIST_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/SET_TO_LIST' A) s))) = (('const/bool/IN' A) x s)))))).
tt('thm/list/SET_TO_LIST_SING_', ax, ![A : $t]: (![x : A]: ((('const/list/SET_TO_LIST' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) = (('const/list/CONS' A) x ('const/list/NIL' A))))).
tt('thm/list/ALL_DISTINCT_SET_TO_LIST_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (('const/list/ALL_DISTINCT' A) (('const/list/SET_TO_LIST' A) s))))).
tt('thm/list/ITSET_eq_FOLDL_SET_TO_LIST_', ax, ![A : $t, B : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > (B > B)), a : B]: ((('const/pred_set/ITSET' A B) f s a) = (('const/list/FOLDL' A B) (('const/combin/C' A B B) f) a (('const/list/SET_TO_LIST' A) s))))))).
tt('thm/list/isPREFIX_0', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/isPREFIX' A) ('const/list/NIL' A) l) = $true))).
tt('thm/list/isPREFIX_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A), l : ('type/list/list' A)]: ((('const/list/isPREFIX' A) (('const/list/CONS' A) h t) l) = (('const/list/list_CASE' A $o) l $false (^['h\'' : A, 't\'' : ('type/list/list' A)]: ((h = 'h\'') & (('const/list/isPREFIX' A) t 't\''))))))).
tt('thm/list/isPREFIX_THM_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/isPREFIX' A) ('const/list/NIL' A) l) = $true))).
tt('thm/list/isPREFIX_THM_1', ax, ![A : $t]: (![t : ('type/list/list' A), h : A]: ((('const/list/isPREFIX' A) (('const/list/CONS' A) h t) ('const/list/NIL' A)) = $false))).
tt('thm/list/isPREFIX_THM_e2', ax, ![A : $t]: (![t2 : ('type/list/list' A), t1 : ('type/list/list' A), h2 : A, h1 : A]: ((('const/list/isPREFIX' A) (('const/list/CONS' A) h1 t1) (('const/list/CONS' A) h2 t2)) = ((h1 = h2) & (('const/list/isPREFIX' A) t1 t2))))).
tt('thm/list/SNOC_0', def, ![A : $t]: (![x : A]: ((('const/list/SNOC' A) x ('const/list/NIL' A)) = (('const/list/CONS' A) x ('const/list/NIL' A))))).
tt('thm/list/SNOC_e1', def, ![A : $t]: (![x : A, 'x\'' : A, l : ('type/list/list' A)]: ((('const/list/SNOC' A) x (('const/list/CONS' A) 'x\'' l)) = (('const/list/CONS' A) 'x\'' (('const/list/SNOC' A) x l))))).
tt('thm/list/LENGTH_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/SNOC' A) x l)) = ('const/num/SUC' (('const/list/LENGTH' A) l))))).
tt('thm/list/LAST_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/LAST' A) (('const/list/SNOC' A) x l)) = x))).
tt('thm/list/FRONT_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/FRONT' A) (('const/list/SNOC' A) x l)) = l))).
tt('thm/list/SNOC_APPEND_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/SNOC' A) x l) = (('const/list/APPEND' A) l (('const/list/CONS' A) x ('const/list/NIL' A)))))).
tt('thm/list/LIST_TO_SET_SNOC_', ax, ![A : $t]: (![x : A, ls : ('type/list/list' A)]: ((('const/list/LIST_TO_SET' A) (('const/list/SNOC' A) x ls)) = (('const/pred_set/INSERT' A) x (('const/list/LIST_TO_SET' A) ls))))).
tt('thm/list/MAP_SNOC_', ax, ![A : $t, B : $t]: (![f : (A > B), x : A, l : ('type/list/list' A)]: ((('const/list/MAP' A B) f (('const/list/SNOC' A) x l)) = (('const/list/SNOC' B) (f x) (('const/list/MAP' A B) f l))))).
tt('thm/list/EL_SNOC_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (![x : A]: ((('const/list/EL' A) n (('const/list/SNOC' A) x l)) = (('const/list/EL' A) n l)))))).
tt('thm/list/EL_LENGTH_SNOC_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A]: ((('const/list/EL' A) (('const/list/LENGTH' A) l) (('const/list/SNOC' A) x l)) = x))).
tt('thm/list/APPEND_SNOC_', ax, ![A : $t]: (![l1 : ('type/list/list' A), x : A, l2 : ('type/list/list' A)]: ((('const/list/APPEND' A) l1 (('const/list/SNOC' A) x l2)) = (('const/list/SNOC' A) x (('const/list/APPEND' A) l1 l2))))).
tt('thm/list/EVERY_SNOC_', ax, ![A : $t]: (![P : (A > $o), x : A, l : ('type/list/list' A)]: ((('const/list/EVERY' A) P (('const/list/SNOC' A) x l)) = ((('const/list/EVERY' A) P l) & (P x))))).
tt('thm/list/EXISTS_SNOC_', ax, ![A : $t]: (![P : (A > $o), x : A, l : ('type/list/list' A)]: ((('const/list/EXISTS' A) P (('const/list/SNOC' A) x l)) = ((P x) | (('const/list/EXISTS' A) P l))))).
tt('thm/list/MEM_SNOC_', ax, ![A : $t]: (![y : A, x : A, l : ('type/list/list' A)]: ((('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) (('const/list/SNOC' A) x l))) = ((y = x) | (('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) l)))))).
tt('thm/list/SNOC_11_', ax, ![A : $t]: (![x : A, y : ('type/list/list' A), a : A, b : ('type/list/list' A)]: (((('const/list/SNOC' A) x y) = (('const/list/SNOC' A) a b)) = ((x = a) & (y = b))))).
tt('thm/list/REVERSE_SNOC_DEF_0', ax, ![B : $t]: ((('const/list/REVERSE' B) ('const/list/NIL' B)) = ('const/list/NIL' B))).
tt('thm/list/REVERSE_SNOC_DEF_e1', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/REVERSE' A) (('const/list/CONS' A) x l)) = (('const/list/SNOC' A) x (('const/list/REVERSE' A) l))))).
tt('thm/list/REVERSE_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/REVERSE' A) (('const/list/SNOC' A) x l)) = (('const/list/CONS' A) x (('const/list/REVERSE' A) l))))).
tt('thm/list/SNOC_Axiom_', ax, ![A : $t, B : $t]: (![e : B, f : (A > (('type/list/list' A) > (B > B)))]: (?[fn : (('type/list/list' A) > B)]: (((fn ('const/list/NIL' A)) = e) & (![x : A, l : ('type/list/list' A)]: ((fn (('const/list/SNOC' A) x l)) = (f x l (fn l)))))))).
tt('thm/list/SNOC_INDUCT_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: (((P ('const/list/NIL' A)) & (![l : ('type/list/list' A)]: ((P l) => (![x : A]: (P (('const/list/SNOC' A) x l)))))) => (![l : ('type/list/list' A)]: (P l))))).
tt('thm/list/SNOC_CASES_', ax, ![A : $t]: (![ll : ('type/list/list' A)]: ((ll = ('const/list/NIL' A)) | (?[x : A, l : ('type/list/list' A)]: (ll = (('const/list/SNOC' A) x l)))))).
tt('thm/list/GENLIST_0', def, ![A : $t]: (![f : ('type/num/num' > A)]: ((('const/list/GENLIST' A) f 'const/num/0') = ('const/list/NIL' A)))).
tt('thm/list/GENLIST_e1', def, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num']: ((('const/list/GENLIST' A) f ('const/num/SUC' n)) = (('const/list/SNOC' A) (f n) (('const/list/GENLIST' A) f n))))).
tt('thm/list/LENGTH_GENLIST_', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num']: ((('const/list/LENGTH' A) (('const/list/GENLIST' A) f n)) = n))).
tt('thm/list/GENLIST_AUX_0', def, ![A : $t]: (![f : ('type/num/num' > A), l : ('type/list/list' A)]: ((('const/list/GENLIST_AUX' A) f 'const/num/0' l) = l))).
tt('thm/list/GENLIST_AUX_e1', def, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/GENLIST_AUX' A) f ('const/num/SUC' n) l) = (('const/list/GENLIST_AUX' A) f n (('const/list/CONS' A) (f n) l))))).
tt('thm/list/GENLIST_AUX_compute_0', ax, ![A : $t]: (![f : ('type/num/num' > A), l : ('type/list/list' A)]: ((('const/list/GENLIST_AUX' A) f 'const/num/0' l) = l))).
tt('thm/list/GENLIST_AUX_compute_1', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/GENLIST_AUX' A) f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) l) = (('const/list/GENLIST_AUX' A) f ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/list/CONS' A) (f ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) l))))).
tt('thm/list/GENLIST_AUX_compute_e2', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/GENLIST_AUX' A) f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) l) = (('const/list/GENLIST_AUX' A) f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/CONS' A) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) l))))).
tt('thm/list/PAD_LEFT_', def, ![A : $t]: (![c : A, n : 'type/num/num', s : ('type/list/list' A)]: ((('const/list/PAD_LEFT' A) c n s) = (('const/list/APPEND' A) (('const/list/GENLIST' A) (('const/combin/K' A 'type/num/num') c) ('const/arithmetic/-' n (('const/list/LENGTH' A) s))) s)))).
tt('thm/list/PAD_RIGHT_', def, ![A : $t]: (![c : A, n : 'type/num/num', s : ('type/list/list' A)]: ((('const/list/PAD_RIGHT' A) c n s) = (('const/list/APPEND' A) s (('const/list/GENLIST' A) (('const/combin/K' A 'type/num/num') c) ('const/arithmetic/-' n (('const/list/LENGTH' A) s))))))).
tt('thm/list/MAP_GENLIST_', ax, ![A : $t, B : $t]: (![f : (A > B), g : ('type/num/num' > A), n : 'type/num/num']: ((('const/list/MAP' A B) f (('const/list/GENLIST' A) g n)) = (('const/list/GENLIST' B) (('const/combin/o' 'type/num/num' B A) f g) n)))).
tt('thm/list/EL_GENLIST_', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' x n) => ((('const/list/EL' A) x (('const/list/GENLIST' A) f n)) = (f x))))).
tt('thm/list/HD_GENLIST_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/list/HD' A) (('const/list/GENLIST' A) f ('const/num/SUC' n))) = (f 'const/num/0')))).
tt('thm/list/HD_GENLIST_COR_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: (('const/prim_rec/<' 'const/num/0' n) => ((('const/list/HD' A) (('const/list/GENLIST' A) f n)) = (f 'const/num/0'))))).
tt('thm/list/GENLIST_FUN_EQ_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A), g : ('type/num/num' > A)]: (((('const/list/GENLIST' A) f n) = (('const/list/GENLIST' A) g n)) = (![x : 'type/num/num']: (('const/prim_rec/<' x n) => ((f x) = (g x))))))).
tt('thm/list/GENLIST_APPEND_', ax, ![A : $t]: (![f : ('type/num/num' > A), a : 'type/num/num', b : 'type/num/num']: ((('const/list/GENLIST' A) f ('const/arithmetic/+' a b)) = (('const/list/APPEND' A) (('const/list/GENLIST' A) f b) (('const/list/GENLIST' A) (^[t : 'type/num/num']: (f ('const/arithmetic/+' t b))) a))))).
tt('thm/list/EVERY_GENLIST_', ax, ![A : $t]: (![f : ('type/num/num' > A), P : (A > $o), n : 'type/num/num']: ((('const/list/EVERY' A) P (('const/list/GENLIST' A) f n)) = (![i : 'type/num/num']: (('const/prim_rec/<' i n) => (P (f i))))))).
tt('thm/list/EXISTS_GENLIST_', ax, ![A : $t]: (![f : ('type/num/num' > A), P : (A > $o), n : 'type/num/num']: ((('const/list/EXISTS' A) P (('const/list/GENLIST' A) f n)) = (?[i : 'type/num/num']: (('const/prim_rec/<' i n) & (P (f i))))))).
tt('thm/list/TL_GENLIST_', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num']: ((('const/list/TL' A) (('const/list/GENLIST' A) f ('const/num/SUC' n))) = (('const/list/GENLIST' A) (('const/combin/o' 'type/num/num' A 'type/num/num') f 'const/num/SUC') n)))).
tt('thm/list/ZIP_GENLIST_', ax, ![B : $t, A : $t]: (![l : ('type/list/list' A), f : ('type/num/num' > B), n : 'type/num/num']: (((('const/list/LENGTH' A) l) = n) => ((('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l (('const/list/GENLIST' B) f n))) = (('const/list/GENLIST' ('type/pair/prod' A B)) (^[x : 'type/num/num']: (('const/pair/,' A B) (('const/list/EL' A) x l) (f x))) n))))).
tt('thm/list/GENLIST_CONS_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/list/GENLIST' A) f ('const/num/SUC' n)) = (('const/list/CONS' A) (f 'const/num/0') (('const/list/GENLIST' A) (('const/combin/o' 'type/num/num' A 'type/num/num') f 'const/num/SUC') n))))).
tt('thm/list/NULL_GENLIST_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/list/NULL' A) (('const/list/GENLIST' A) f n)) = (n = 'const/num/0')))).
tt('thm/list/GENLIST_GENLIST_AUX_', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num']: ((('const/list/GENLIST' A) f n) = (('const/list/GENLIST_AUX' A) f n ('const/list/NIL' A))))).
tt('thm/list/GENLIST_NUMERALS_0', ax, ![A : $t]: (![f : ('type/num/num' > A)]: ((('const/list/GENLIST' A) f 'const/num/0') = ('const/list/NIL' A)))).
tt('thm/list/GENLIST_NUMERALS_e1', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/list/GENLIST' A) f ('const/arithmetic/NUMERAL' n)) = (('const/list/GENLIST_AUX' A) f ('const/arithmetic/NUMERAL' n) ('const/list/NIL' A))))).
tt('thm/list/MEM_GENLIST_', ax, ![A : $t]: (![x : A, n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/GENLIST' A) f n))) = (?[m : 'type/num/num']: (('const/prim_rec/<' m n) & (x = (f m))))))).
tt('thm/list/ALL_DISTINCT_SNOC_', ax, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) (('const/list/SNOC' A) x l)) = ((~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l))) & (('const/list/ALL_DISTINCT' A) l))))).
tt('thm/list/ALL_DISTINCT_GENLIST_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/list/ALL_DISTINCT' A) (('const/list/GENLIST' A) f n)) = (![m1 : 'type/num/num', m2 : 'type/num/num']: ((('const/prim_rec/<' m1 n) & (('const/prim_rec/<' m2 n) & ((f m1) = (f m2)))) => (m1 = m2)))))).
tt('thm/list/FOLDL_SNOC_', ax, ![A : $t, B : $t]: (![f : (B > (A > B)), e : B, x : A, l : ('type/list/list' A)]: ((('const/list/FOLDL' A B) f e (('const/list/SNOC' A) x l)) = (f (('const/list/FOLDL' A B) f e l) x)))).
tt('thm/list/SUM_SNOC_', ax, (![x : 'type/num/num', l : ('type/list/list' 'type/num/num')]: (('const/list/SUM' (('const/list/SNOC' 'type/num/num') x l)) = ('const/arithmetic/+' ('const/list/SUM' l) x)))).
tt('thm/list/SUM_APPEND_', ax, (![l1 : ('type/list/list' 'type/num/num'), l2 : ('type/list/list' 'type/num/num')]: (('const/list/SUM' (('const/list/APPEND' 'type/num/num') l1 l2)) = ('const/arithmetic/+' ('const/list/SUM' l1) ('const/list/SUM' l2))))).
tt('thm/list/SUM_MAP_FOLDL_', ax, ![A : $t]: (![f : (A > 'type/num/num'), ls : ('type/list/list' A)]: (('const/list/SUM' (('const/list/MAP' A 'type/num/num') f ls)) = (('const/list/FOLDL' A 'type/num/num') (^[a : 'type/num/num', e : A]: ('const/arithmetic/+' a (f e))) 'const/num/0' ls)))).
tt('thm/list/SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST_', ax, ![A : $t]: (![s : (A > $o), f : (A > 'type/num/num')]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/SUM_IMAGE' A) f s) = ('const/list/SUM' (('const/list/MAP' A 'type/num/num') f (('const/list/SET_TO_LIST' A) s))))))).
tt('thm/list/EL_REVERSE_', 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/list/EL' A) ('const/prim_rec/PRE' ('const/arithmetic/-' (('const/list/LENGTH' A) l) n)) l))))).
tt('thm/list/REVERSE_GENLIST_', ax, ![A : $t]: (![n : 'type/num/num', f : ('type/num/num' > A)]: ((('const/list/REVERSE' A) (('const/list/GENLIST' A) f n)) = (('const/list/GENLIST' A) (^[m : 'type/num/num']: (f ('const/arithmetic/-' ('const/prim_rec/PRE' n) m))) n)))).
tt('thm/list/FOLDL_UNION_BIGUNION_', ax, ![A : $t, B : $t]: (![f : (A > (B > $o)), ls : ('type/list/list' A), s : (B > $o)]: ((('const/list/FOLDL' A (B > $o)) (^[s0 : (B > $o), x : A]: (('const/pred_set/UNION' B) s0 (f x))) s ls) = (('const/pred_set/UNION' B) s (('const/pred_set/BIGUNION' B) (('const/pred_set/IMAGE' A (B > $o)) f (('const/list/LIST_TO_SET' A) ls))))))).
tt('thm/list/FOLDL_UNION_BIGUNION_paired_', ax, ![A : $t, B : $t, C : $t]: (![f : (A > (B > (C > $o))), ls : ('type/list/list' ('type/pair/prod' A B)), s : (C > $o)]: ((('const/list/FOLDL' ('type/pair/prod' A B) (C > $o)) (^[s0 : (C > $o)]: (('const/pair/UNCURRY' A B (C > $o)) (^[x : A, y : B]: (('const/pred_set/UNION' C) s0 (f x y))))) s ls) = (('const/pred_set/UNION' C) s (('const/pred_set/BIGUNION' C) (('const/pred_set/IMAGE' ('type/pair/prod' A B) (C > $o)) (('const/pair/UNCURRY' A B (C > $o)) f) (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) ls))))))).
tt('thm/list/FOLDL_ZIP_SAME_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' A), f : (B > (('type/pair/prod' A A) > B)), e : B]: ((('const/list/FOLDL' ('type/pair/prod' A A) B) f e (('const/list/ZIP' A A) (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) ls ls))) = (('const/list/FOLDL' A B) (^[x : B, y : A]: (f x (('const/pair/,' A A) y y))) e ls)))).
tt('thm/list/MAP_ZIP_SAME_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' A), f : (('type/pair/prod' A A) > B)]: ((('const/list/MAP' ('type/pair/prod' A A) B) f (('const/list/ZIP' A A) (('const/pair/,' ('type/list/list' A) ('type/list/list' A)) ls ls))) = (('const/list/MAP' A B) (^[x : A]: (f (('const/pair/,' A A) x x))) ls)))).
tt('thm/list/INFINITE_LIST_UNIV_', ax, ![A : $t]: (~ (('const/pred_set/FINITE' ('type/list/list' A)) ('const/pred_set/UNIV' ('type/list/list' A))))).
tt('thm/list/LEN_DEF_0', def, ![A : $t]: (![n : 'type/num/num']: ((('const/list/LEN' A) ('const/list/NIL' A) n) = n))).
tt('thm/list/LEN_DEF_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A), n : 'type/num/num']: ((('const/list/LEN' A) (('const/list/CONS' A) h t) n) = (('const/list/LEN' A) t ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/list/REV_DEF_0', def, ![A : $t]: (![acc : ('type/list/list' A)]: ((('const/list/REV' A) ('const/list/NIL' A) acc) = acc))).
tt('thm/list/REV_DEF_e1', def, ![A : $t]: (![h : A, t : ('type/list/list' A), acc : ('type/list/list' A)]: ((('const/list/REV' A) (('const/list/CONS' A) h t) acc) = (('const/list/REV' A) t (('const/list/CONS' A) h acc))))).
tt('thm/list/LEN_LENGTH_LEM_', ax, ![A : $t]: (![L : ('type/list/list' A), n : 'type/num/num']: ((('const/list/LEN' A) L n) = ('const/arithmetic/+' (('const/list/LENGTH' A) L) n)))).
tt('thm/list/REV_REVERSE_LEM_', ax, ![A : $t]: (![L1 : ('type/list/list' A), L2 : ('type/list/list' A)]: ((('const/list/REV' A) L1 L2) = (('const/list/APPEND' A) (('const/list/REVERSE' A) L1) L2)))).
tt('thm/list/LENGTH_LEN_', ax, ![A : $t]: (![L : ('type/list/list' A)]: ((('const/list/LENGTH' A) L) = (('const/list/LEN' A) L 'const/num/0')))).
tt('thm/list/REVERSE_REV_', ax, ![A : $t]: (![L : ('type/list/list' A)]: ((('const/list/REVERSE' A) L) = (('const/list/REV' A) L ('const/list/NIL' A))))).
tt('thm/list/SUM_ACC_DEF_0', def, (![acc : 'type/num/num']: (('const/list/SUM_ACC' ('const/list/NIL' 'type/num/num') acc) = acc))).
tt('thm/list/SUM_ACC_DEF_e1', def, (![h : 'type/num/num', t : ('type/list/list' 'type/num/num'), acc : 'type/num/num']: (('const/list/SUM_ACC' (('const/list/CONS' 'type/num/num') h t) acc) = ('const/list/SUM_ACC' t ('const/arithmetic/+' h acc))))).
tt('thm/list/SUM_ACC_SUM_LEM_', ax, (![L : ('type/list/list' 'type/num/num'), n : 'type/num/num']: (('const/list/SUM_ACC' L n) = ('const/arithmetic/+' ('const/list/SUM' L) n)))).
tt('thm/list/SUM_SUM_ACC_', ax, (![L : ('type/list/list' 'type/num/num')]: (('const/list/SUM' L) = ('const/list/SUM_ACC' L 'const/num/0')))).
tt('thm/list/EXISTS_LIST_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: ((?[l : ('type/list/list' A)]: (P l)) = ((P ('const/list/NIL' A)) | (?[h : A, t : ('type/list/list' A)]: (P (('const/list/CONS' A) h t))))))).
tt('thm/list/FORALL_LIST_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: ((![l : ('type/list/list' A)]: (P l)) = ((P ('const/list/NIL' A)) & (![h : A, t : ('type/list/list' A)]: (P (('const/list/CONS' A) h t))))))).
tt('thm/list/MEM_SPLIT_APPEND_first_', ax, ![A : $t]: (![l : ('type/list/list' A), e : A]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)) = (?[pfx : ('type/list/list' A), sfx : ('type/list/list' A)]: ((l = (('const/list/APPEND' A) (('const/list/APPEND' A) pfx (('const/list/CONS' A) e ('const/list/NIL' A))) sfx)) & (~ (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) pfx)))))))).
tt('thm/list/MEM_SPLIT_APPEND_last_', ax, ![A : $t]: (![l : ('type/list/list' A), e : A]: ((('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) l)) = (?[pfx : ('type/list/list' A), sfx : ('type/list/list' A)]: ((l = (('const/list/APPEND' A) (('const/list/APPEND' A) pfx (('const/list/CONS' A) e ('const/list/NIL' A))) sfx)) & (~ (('const/bool/IN' A) e (('const/list/LIST_TO_SET' A) sfx)))))))).
tt('thm/list/APPEND_EQ_APPEND_', ax, ![A : $t]: (![m2 : ('type/list/list' A), m1 : ('type/list/list' A), l2 : ('type/list/list' A), l1 : ('type/list/list' A)]: (((('const/list/APPEND' A) l1 l2) = (('const/list/APPEND' A) m1 m2)) = ((?[l : ('type/list/list' A)]: ((l1 = (('const/list/APPEND' A) m1 l)) & (m2 = (('const/list/APPEND' A) l l2)))) | (?[l : ('type/list/list' A)]: ((m1 = (('const/list/APPEND' A) l1 l)) & (l2 = (('const/list/APPEND' A) l m2)))))))).
tt('thm/list/APPEND_EQ_CONS_', ax, ![A : $t]: (![t : ('type/list/list' A), l2 : ('type/list/list' A), l1 : ('type/list/list' A), h : A]: (((('const/list/APPEND' A) l1 l2) = (('const/list/CONS' A) h t)) = (((l1 = ('const/list/NIL' A)) & (l2 = (('const/list/CONS' A) h t))) | (?[lt : ('type/list/list' A)]: ((l1 = (('const/list/CONS' A) h lt)) & (t = (('const/list/APPEND' A) lt l2)))))))).
tt('thm/list/APPEND_EQ_APPEND_MID_', ax, ![A : $t]: (![m2 : ('type/list/list' A), m1 : ('type/list/list' A), l2 : ('type/list/list' A), l1 : ('type/list/list' A), e : A]: (((('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) e ('const/list/NIL' A))) l2) = (('const/list/APPEND' A) m1 m2)) = ((?[l : ('type/list/list' A)]: ((m1 = (('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) e ('const/list/NIL' A))) l)) & (l2 = (('const/list/APPEND' A) l m2)))) | (?[l : ('type/list/list' A)]: ((l1 = (('const/list/APPEND' A) m1 l)) & (m2 = (('const/list/APPEND' A) (('const/list/APPEND' A) l (('const/list/CONS' A) e ('const/list/NIL' A))) l2)))))))).
tt('thm/list/LUPDATE_def_0', def, ![A : $t]: (![e : A, n : 'type/num/num']: ((('const/list/LUPDATE' A) e n ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/LUPDATE_def_1', def, ![A : $t]: (![e : A, x : A, l : ('type/list/list' A)]: ((('const/list/LUPDATE' A) e 'const/num/0' (('const/list/CONS' A) x l)) = (('const/list/CONS' A) e l)))).
tt('thm/list/LUPDATE_def_e2', def, ![A : $t]: (![e : A, n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/list/LUPDATE' A) e ('const/num/SUC' n) (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/list/LUPDATE' A) e n l))))).
tt('thm/list/LUPDATE_SEM_0', ax, ![A : $t]: (![e : A, n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/LUPDATE' A) e n l)) = (('const/list/LENGTH' A) l)))).
tt('thm/list/LUPDATE_SEM_e1', ax, ![A : $t]: (![e : A, n : 'type/num/num', l : ('type/list/list' A), p : 'type/num/num']: (('const/prim_rec/<' p (('const/list/LENGTH' A) l)) => ((('const/list/EL' A) p (('const/list/LUPDATE' A) e n l)) = (('const/bool/COND' A) (p = n) e (('const/list/EL' A) p l)))))).
tt('thm/list/EL_LUPDATE_', ax, ![A : $t]: (![ys : ('type/list/list' A), x : A, i : 'type/num/num', k : 'type/num/num']: ((('const/list/EL' A) i (('const/list/LUPDATE' A) x k ys)) = (('const/bool/COND' A) ((i = k) & ('const/prim_rec/<' k (('const/list/LENGTH' A) ys))) x (('const/list/EL' A) i ys))))).
tt('thm/list/LENGTH_LUPDATE_', ax, ![A : $t]: (![x : A, n : 'type/num/num', ys : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/LUPDATE' A) x n ys)) = (('const/list/LENGTH' A) ys)))).
tt('thm/list/LUPDATE_LENGTH_', ax, ![A : $t]: (![xs : ('type/list/list' A), x : A, y : A, ys : ('type/list/list' A)]: ((('const/list/LUPDATE' A) x (('const/list/LENGTH' A) xs) (('const/list/APPEND' A) xs (('const/list/CONS' A) y ys))) = (('const/list/APPEND' A) xs (('const/list/CONS' A) x ys))))).
tt('thm/list/LUPDATE_SNOC_', ax, ![A : $t]: (![ys : ('type/list/list' A), k : 'type/num/num', x : A, y : A]: ((('const/list/LUPDATE' A) x k (('const/list/SNOC' A) y ys)) = (('const/bool/COND' ('type/list/list' A)) (k = (('const/list/LENGTH' A) ys)) (('const/list/SNOC' A) x ys) (('const/list/SNOC' A) y (('const/list/LUPDATE' A) x k ys)))))).
tt('thm/list/MEM_LUPDATE_E_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A, y : A, i : 'type/num/num']: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/LUPDATE' A) y i l))) => ((x = y) | (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)))))).
tt('thm/list/MEM_LUPDATE_', ax, ![A : $t]: (![l : ('type/list/list' A), x : A, y : A, i : 'type/num/num']: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/LUPDATE' A) y i l))) = ((('const/prim_rec/<' i (('const/list/LENGTH' A) l)) & (x = y)) | (?[j : 'type/num/num']: (('const/prim_rec/<' j (('const/list/LENGTH' A) l)) & ((~ (i = j)) & ((('const/list/EL' A) j l) = x)))))))).
tt('thm/list/LUPDATE_compute_0', ax, ![A : $t]: (![e : A, n : 'type/num/num']: ((('const/list/LUPDATE' A) e n ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/LUPDATE_compute_1', ax, ![A : $t]: (![e : A, x : A, l : ('type/list/list' A)]: ((('const/list/LUPDATE' A) e 'const/num/0' (('const/list/CONS' A) x l)) = (('const/list/CONS' A) e l)))).
tt('thm/list/LUPDATE_compute_2', ax, ![A : $t]: (![e : A, n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/list/LUPDATE' A) e ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/list/LUPDATE' A) e ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) l))))).
tt('thm/list/LUPDATE_compute_e3', ax, ![A : $t]: (![e : A, n : 'type/num/num', x : A, l : ('type/list/list' A)]: ((('const/list/LUPDATE' A) e ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) (('const/list/CONS' A) x l)) = (('const/list/CONS' A) x (('const/list/LUPDATE' A) e ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) l))))).
tt('thm/list/LUPDATE_MAP_', ax, ![A : $t, B : $t]: (![x : A, n : 'type/num/num', l : ('type/list/list' A), f : (A > B)]: ((('const/list/MAP' A B) f (('const/list/LUPDATE' A) x n l)) = (('const/list/LUPDATE' B) (f x) n (('const/list/MAP' A B) f l))))).
tt('thm/list/EVERYi_DEF_0', def, ![A : $t]: (![P : ('type/num/num' > (A > $o))]: ((('const/list/EVERYi' A) P ('const/list/NIL' A)) = $true))).
tt('thm/list/EVERYi_DEF_e1', def, ![A : $t]: (![P : ('type/num/num' > (A > $o)), h : A, t : ('type/list/list' A)]: ((('const/list/EVERYi' A) P (('const/list/CONS' A) h t)) = ((P 'const/num/0' h) & (('const/list/EVERYi' A) (('const/combin/o' 'type/num/num' (A > $o) 'type/num/num') P 'const/num/SUC') t))))).
tt('thm/list/splitAtPki_DEF_0', def, ![B : $t, A : $t]: (![P : ('type/num/num' > (B > $o)), k : (('type/list/list' B) > (('type/list/list' B) > A))]: ((('const/list/splitAtPki' A B) P k ('const/list/NIL' B)) = (k ('const/list/NIL' B) ('const/list/NIL' B))))).
tt('thm/list/splitAtPki_DEF_e1', def, ![B : $t, A : $t]: (![P : ('type/num/num' > (B > $o)), k : (('type/list/list' B) > (('type/list/list' B) > A)), h : B, t : ('type/list/list' B)]: ((('const/list/splitAtPki' A B) P k (('const/list/CONS' B) h t)) = (('const/bool/COND' A) (P 'const/num/0' h) (k ('const/list/NIL' B) (('const/list/CONS' B) h t)) (('const/list/splitAtPki' A B) (('const/combin/o' 'type/num/num' (B > $o) 'type/num/num') P 'const/num/SUC') (^[p : ('type/list/list' B), s : ('type/list/list' B)]: (k (('const/list/CONS' B) h p) s)) t))))).
tt('thm/list/splitAtPki_APPEND_', ax, ![A : $t, B : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A), P : ('type/num/num' > (A > $o)), k : (('type/list/list' A) > (('type/list/list' A) > B))]: (((('const/list/EVERYi' A) (^[i : 'type/num/num']: (('const/combin/o' A $o $o) $not (P i))) l1) & (('const/prim_rec/<' 'const/num/0' (('const/list/LENGTH' A) l2)) => (P (('const/list/LENGTH' A) l1) (('const/list/HD' A) l2)))) => ((('const/list/splitAtPki' B A) P k (('const/list/APPEND' A) l1 l2)) = (k l1 l2))))).
tt('thm/list/splitAtPki_EQN_', ax, ![B : $t, A : $t]: (![l : ('type/list/list' B), k : (('type/list/list' B) > (('type/list/list' B) > A)), P : ('type/num/num' > (B > $o))]: ((('const/list/splitAtPki' A B) P k l) = (('const/option/option_CASE' 'type/num/num' A) ('const/while/OLEAST' (^[i : 'type/num/num']: (('const/prim_rec/<' i (('const/list/LENGTH' B) l)) & (P i (('const/list/EL' B) i l))))) (k l ('const/list/NIL' B)) (^[i : 'type/num/num']: (k (('const/list/TAKE' B) i l) (('const/list/DROP' B) i l))))))).
tt('thm/list/TAKE_LENGTH_TOO_LONG_', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l) n) => ((('const/list/TAKE' A) n l) = l)))).
tt('thm/list/DROP_LENGTH_TOO_LONG_', ax, ![A : $t]: (![l : ('type/list/list' A), n : 'type/num/num']: (('const/arithmetic/<=' (('const/list/LENGTH' A) l) n) => ((('const/list/DROP' A) n l) = ('const/list/NIL' A))))).
tt('thm/list/TAKE_splitAtPki_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/TAKE' A) n l) = (('const/list/splitAtPki' ('type/list/list' A) A) (('const/combin/o' 'type/num/num' (A > $o) $o) ('const/combin/K' $o A) (($equals 'type/num/num') n)) ('const/combin/K' ('type/list/list' A) ('type/list/list' A)) l)))).
tt('thm/list/DROP_splitAtPki_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/list/DROP' A) n l) = (('const/list/splitAtPki' ('type/list/list' A) A) (('const/combin/o' 'type/num/num' (A > $o) $o) ('const/combin/K' $o A) (($equals 'type/num/num') n)) (('const/combin/K' (('type/list/list' A) > ('type/list/list' A)) ('type/list/list' A)) ('const/combin/I' ('type/list/list' A))) l)))).
tt('thm/list/LIST_BIND_DEF_', def, ![B : $t, A : $t]: (![l : ('type/list/list' B), f : (B > ('type/list/list' A))]: ((('const/list/LIST_BIND' A B) l f) = (('const/list/FLAT' A) (('const/list/MAP' B ('type/list/list' A)) f l))))).
tt('thm/list/LIST_BIND_THM_0', ax, ![A : $t, B : $t]: (![f : (B > ('type/list/list' A))]: ((('const/list/LIST_BIND' A B) ('const/list/NIL' B) f) = ('const/list/NIL' A)))).
tt('thm/list/LIST_BIND_THM_e1', ax, ![B : $t, A : $t]: (![t : ('type/list/list' B), h : B, f : (B > ('type/list/list' A))]: ((('const/list/LIST_BIND' A B) (('const/list/CONS' B) h t) f) = (('const/list/APPEND' A) (f h) (('const/list/LIST_BIND' A B) t f))))).
tt('thm/list/LIST_IGNORE_BIND_DEF_', def, ![A : $t, B : $t]: (![m1 : ('type/list/list' B), m2 : ('type/list/list' A)]: ((('const/list/LIST_IGNORE_BIND' A B) m1 m2) = (('const/list/LIST_BIND' A B) m1 (('const/combin/K' ('type/list/list' A) B) m2))))).
tt('thm/list/LIST_BIND_ID_0', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/LIST_BIND' A ('type/list/list' A)) l (^[x : ('type/list/list' A)]: x)) = (('const/list/FLAT' A) l)))).
tt('thm/list/LIST_BIND_ID_e1', ax, ![A : $t]: (![l : ('type/list/list' ('type/list/list' A))]: ((('const/list/LIST_BIND' A ('type/list/list' A)) l ('const/combin/I' ('type/list/list' A))) = (('const/list/FLAT' A) l)))).
tt('thm/list/LIST_BIND_APPEND_', ax, ![B : $t, A : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' B), f : (B > ('type/list/list' A))]: ((('const/list/LIST_BIND' A B) (('const/list/APPEND' B) l1 l2) f) = (('const/list/APPEND' A) (('const/list/LIST_BIND' A B) l1 f) (('const/list/LIST_BIND' A B) l2 f))))).
tt('thm/list/LIST_BIND_MAP_', ax, ![C : $t, B : $t, A : $t]: (![l : ('type/list/list' C), g : (B > ('type/list/list' A)), f : (C > B)]: ((('const/list/LIST_BIND' A B) (('const/list/MAP' C B) f l) g) = (('const/list/LIST_BIND' A C) l (('const/combin/o' C ('type/list/list' A) B) g f))))).
tt('thm/list/MAP_LIST_BIND_', ax, ![C : $t, B : $t, A : $t]: (![l : ('type/list/list' C), g : (C > ('type/list/list' B)), f : (B > A)]: ((('const/list/MAP' B A) f (('const/list/LIST_BIND' B C) l g)) = (('const/list/LIST_BIND' A C) l (('const/combin/o' C ('type/list/list' A) ('type/list/list' B)) (('const/list/MAP' B A) f) g))))).
tt('thm/list/LIST_BIND_LIST_BIND_', ax, ![C : $t, B : $t, A : $t]: (![l : ('type/list/list' C), g : (C > ('type/list/list' B)), f : (B > ('type/list/list' A))]: ((('const/list/LIST_BIND' A B) (('const/list/LIST_BIND' B C) l g) f) = (('const/list/LIST_BIND' A C) l (('const/combin/o' C ('type/list/list' A) ('type/list/list' B)) (('const/combin/C' ('type/list/list' B) (B > ('type/list/list' A)) ('type/list/list' A)) ('const/list/LIST_BIND' A B) f) g))))).
tt('thm/list/SINGL_LIST_APPLY_L_', ax, ![B : $t, A : $t]: (![x : B, f : (B > ('type/list/list' A))]: ((('const/list/LIST_BIND' A B) (('const/list/CONS' B) x ('const/list/NIL' B)) f) = (f x)))).
tt('thm/list/SINGL_LIST_APPLY_R_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/LIST_BIND' A A) l (^[x : A]: (('const/list/CONS' A) x ('const/list/NIL' A)))) = l))).
tt('thm/list/LIST_APPLY_DEF_', def, ![B : $t, A : $t]: (![fs : ('type/list/list' (B > A)), xs : ('type/list/list' B)]: ((('const/list/LIST_APPLY' A B) fs xs) = (('const/list/LIST_BIND' A (B > A)) fs (('const/combin/C' (B > A) ('type/list/list' B) ('type/list/list' A)) ('const/list/MAP' B A) xs))))).
tt('thm/list/LIST_LIFT2_DEF_', def, ![C : $t, B : $t, A : $t]: (![f : (B > (C > A)), xs : ('type/list/list' B), ys : ('type/list/list' C)]: ((('const/list/LIST_LIFT2' A B C) f xs ys) = (('const/list/LIST_APPLY' A C) (('const/list/MAP' B (C > A)) f xs) ys)))).
tt('thm/list/SINGL_APPLY_MAP_', ax, ![B : $t, A : $t]: (![l : ('type/list/list' B), f : (B > A)]: ((('const/list/LIST_APPLY' A B) (('const/list/CONS' (B > A)) f ('const/list/NIL' (B > A))) l) = (('const/list/MAP' B A) f l)))).
tt('thm/list/SINGL_SINGL_APPLY_', ax, ![A : $t, B : $t]: (![x : B, f : (B > A)]: ((('const/list/LIST_APPLY' A B) (('const/list/CONS' (B > A)) f ('const/list/NIL' (B > A))) (('const/list/CONS' B) x ('const/list/NIL' B))) = (('const/list/CONS' A) (f x) ('const/list/NIL' A))))).
tt('thm/list/SINGL_APPLY_PERMUTE_', ax, ![B : $t, A : $t]: (![x : B, fs : ('type/list/list' (B > A))]: ((('const/list/LIST_APPLY' A B) fs (('const/list/CONS' B) x ('const/list/NIL' B))) = (('const/list/LIST_APPLY' A (B > A)) (('const/list/CONS' ((B > A) > A)) (^[f : (B > A)]: (f x)) ('const/list/NIL' ((B > A) > A))) fs)))).
tt('thm/list/MAP_FLAT_', ax, ![B : $t, A : $t]: (![l : ('type/list/list' ('type/list/list' B)), f : (B > A)]: ((('const/list/MAP' B A) f (('const/list/FLAT' B) l)) = (('const/list/FLAT' A) (('const/list/MAP' ('type/list/list' B) ('type/list/list' A)) (('const/list/MAP' B A) f) l))))).
tt('thm/list/LIST_APPLY_o_', ax, ![B : $t, C : $t, A : $t]: (![xs : ('type/list/list' B), gs : ('type/list/list' (B > C)), fs : ('type/list/list' (C > A))]: ((('const/list/LIST_APPLY' A B) (('const/list/LIST_APPLY' (B > A) (B > C)) (('const/list/LIST_APPLY' ((B > C) > (B > A)) (C > A)) (('const/list/CONS' ((C > A) > ((B > C) > (B > A)))) ('const/combin/o' B A C) ('const/list/NIL' ((C > A) > ((B > C) > (B > A))))) fs) gs) xs) = (('const/list/LIST_APPLY' A C) fs (('const/list/LIST_APPLY' C B) gs xs))))).
tt('thm/list/LLEX_DEF_0', def, ![A : $t]: (![R : (A > (A > $o)), l2 : ('type/list/list' A)]: ((('const/list/LLEX' A) R ('const/list/NIL' A) l2) = (~ (l2 = ('const/list/NIL' A)))))).
tt('thm/list/LLEX_DEF_e1', def, ![A : $t]: (![R : (A > (A > $o)), h1 : A, t1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/LLEX' A) R (('const/list/CONS' A) h1 t1) l2) = (('const/list/list_CASE' A $o) l2 $false (^[h2 : A, t2 : ('type/list/list' A)]: (('const/bool/COND' $o) (R h1 h2) $true (('const/bool/COND' $o) (h1 = h2) (('const/list/LLEX' A) R t1 t2) $false))))))).
tt('thm/list/LLEX_THM_tLL', ax, ![A : $t]: (![R : (A > (A > $o))]: (~ (('const/list/LLEX' A) R ('const/list/NIL' A) ('const/list/NIL' A))))).
tt('thm/list/LLEX_THM_tRL', ax, ![A : $t]: (![t1 : ('type/list/list' A), h1 : A, R : (A > (A > $o))]: (~ (('const/list/LLEX' A) R (('const/list/CONS' A) h1 t1) ('const/list/NIL' A))))).
tt('thm/list/LLEX_THM_1', ax, ![A : $t]: (![t2 : ('type/list/list' A), h2 : A, R : (A > (A > $o))]: (('const/list/LLEX' A) R ('const/list/NIL' A) (('const/list/CONS' A) h2 t2)))).
tt('thm/list/LLEX_THM_e2', ax, ![A : $t]: (![t2 : ('type/list/list' A), t1 : ('type/list/list' A), h2 : A, h1 : A, R : (A > (A > $o))]: ((('const/list/LLEX' A) R (('const/list/CONS' A) h1 t1) (('const/list/CONS' A) h2 t2)) = ((R h1 h2) | ((h1 = h2) & (('const/list/LLEX' A) R t1 t2)))))).
tt('thm/list/LLEX_NIL2_', ax, ![A : $t]: (![l : ('type/list/list' A), R : (A > (A > $o))]: (~ (('const/list/LLEX' A) R l ('const/list/NIL' A))))).
tt('thm/list/LLEX_transitive_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/relation/transitive' A) R) => (('const/relation/transitive' ('type/list/list' A)) (('const/list/LLEX' A) R))))).
tt('thm/list/LLEX_total_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/relation/total' A) (('const/relation/RC' A) R)) => (('const/relation/total' ('type/list/list' A)) (('const/relation/RC' ('type/list/list' A)) (('const/list/LLEX' A) R)))))).
tt('thm/list/LLEX_not_WF_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((?[a : A, b : A]: (R a b)) => (~ (('const/relation/WF' ('type/list/list' A)) (('const/list/LLEX' A) R)))))).
tt('thm/list/nub_def_0', def, ![A : $t]: ((('const/list/nub' A) ('const/list/NIL' A)) = ('const/list/NIL' A))).
tt('thm/list/nub_def_e1', def, ![A : $t]: (![x : A, l : ('type/list/list' A)]: ((('const/list/nub' A) (('const/list/CONS' A) x l)) = (('const/bool/COND' ('type/list/list' A)) (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) (('const/list/nub' A) l) (('const/list/CONS' A) x (('const/list/nub' A) l)))))).
tt('thm/list/nub_set_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/LIST_TO_SET' A) (('const/list/nub' A) l)) = (('const/list/LIST_TO_SET' A) l)))).
tt('thm/list/all_distinct_nub_', ax, ![A : $t]: (![l : ('type/list/list' A)]: (('const/list/ALL_DISTINCT' A) (('const/list/nub' A) l)))).
tt('thm/list/nub_append_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/nub' A) (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/list/nub' A) (('const/list/FILTER' A) (^[x : A]: (~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l2)))) l1)) (('const/list/nub' A) l2))))).
tt('thm/list/list_to_set_diff_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/pred_set/DIFF' A) (('const/list/LIST_TO_SET' A) l2) (('const/list/LIST_TO_SET' A) l1)) = (('const/list/LIST_TO_SET' A) (('const/list/FILTER' A) (^[x : A]: (~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l1)))) l2))))).
tt('thm/list/length_nub_append_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/LENGTH' A) (('const/list/nub' A) (('const/list/APPEND' A) l1 l2))) = ('const/arithmetic/+' (('const/list/LENGTH' A) (('const/list/nub' A) l1)) (('const/list/LENGTH' A) (('const/list/nub' A) (('const/list/FILTER' A) (^[x : A]: (~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l1)))) l2))))))).
tt('thm/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/list/EXISTS_LIST_EQ_MAP_', ax, ![B : $t, A : $t]: (![ls : ('type/list/list' A), f : (B > A)]: ((('const/list/EVERY' A) (^[x : A]: (?[y : B]: (x = (f y)))) ls) => (?[l : ('type/list/list' B)]: (ls = (('const/list/MAP' B A) f l)))))).
tt('thm/list/LIST_TO_SET_FLAT_', ax, ![A : $t]: (![ls : ('type/list/list' ('type/list/list' A))]: ((('const/list/LIST_TO_SET' A) (('const/list/FLAT' A) ls)) = (('const/pred_set/BIGUNION' A) (('const/list/LIST_TO_SET' (A > $o)) (('const/list/MAP' ('type/list/list' A) (A > $o)) ('const/list/LIST_TO_SET' A) ls)))))).
tt('thm/list/MEM_APPEND_lemma_', ax, ![A : $t]: (![a : ('type/list/list' A), b : ('type/list/list' A), c : ('type/list/list' A), d : ('type/list/list' A), x : A]: ((((('const/list/APPEND' A) (('const/list/APPEND' A) a (('const/list/CONS' A) x ('const/list/NIL' A))) b) = (('const/list/APPEND' A) (('const/list/APPEND' A) c (('const/list/CONS' A) x ('const/list/NIL' A))) d)) & ((~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) b))) & (~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) a))))) => ((a = c) & (b = d))))).
tt('thm/list/EVERY2_REVERSE_', 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 l2) => (('const/list/LIST_REL' A B) R (('const/list/REVERSE' A) l1) (('const/list/REVERSE' B) l2))))).
tt('thm/list/SUM_MAP_PLUS_', ax, ![A : $t]: (![f : (A > 'type/num/num'), g : (A > 'type/num/num'), ls : ('type/list/list' A)]: (('const/list/SUM' (('const/list/MAP' A 'type/num/num') (^[x : A]: ('const/arithmetic/+' (f x) (g x))) ls)) = ('const/arithmetic/+' ('const/list/SUM' (('const/list/MAP' A 'type/num/num') f ls)) ('const/list/SUM' (('const/list/MAP' A 'type/num/num') g ls)))))).
tt('thm/list/TAKE_LENGTH_ID_rwt_', ax, ![A : $t]: (![l : ('type/list/list' A), m : 'type/num/num']: ((m = (('const/list/LENGTH' A) l)) => ((('const/list/TAKE' A) m l) = l)))).
tt('thm/list/ZIP_DROP_', ax, ![B : $t, A : $t]: (![a : ('type/list/list' A), b : ('type/list/list' B), n : 'type/num/num']: ((('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/DROP' A) n a) (('const/list/DROP' B) n b))) = (('const/list/DROP' ('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/list/GENLIST_EL_', ax, ![A : $t]: (![ls : ('type/list/list' A), f : ('type/num/num' > A), n : 'type/num/num']: (((n = (('const/list/LENGTH' A) ls)) & (![i : 'type/num/num']: (('const/prim_rec/<' i n) => ((f i) = (('const/list/EL' A) i ls))))) => ((('const/list/GENLIST' A) f n) = ls)))).
tt('thm/list/EVERY2_trans_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((![x : A, y : A, z : A]: (((R x y) & (R y z)) => (R x z))) => (![x : ('type/list/list' A), y : ('type/list/list' A), z : ('type/list/list' A)]: (((('const/list/LIST_REL' A A) R x y) & (('const/list/LIST_REL' A A) R y z)) => (('const/list/LIST_REL' A A) R x z)))))).
tt('thm/list/EVERY2_sym_', ax, ![A : $t, B : $t]: (![R2 : (B > (A > $o)), R1 : (A > (B > $o))]: ((![x : A, y : B]: ((R1 x y) => (R2 y x))) => (![x : ('type/list/list' A), y : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) R1 x y) => (('const/list/LIST_REL' B A) R2 y x)))))).
tt('thm/list/EVERY2_LUPDATE_same_', ax, ![B : $t, A : $t]: (![P : (A > (B > $o)), l1 : ('type/list/list' A), l2 : ('type/list/list' B), v1 : A, v2 : B, n : 'type/num/num']: (((P v1 v2) & (('const/list/LIST_REL' A B) P l1 l2)) => (('const/list/LIST_REL' A B) P (('const/list/LUPDATE' A) v1 n l1) (('const/list/LUPDATE' B) v2 n l2))))).
tt('thm/list/EVERY2_refl_', ax, ![A : $t]: (![ls : ('type/list/list' A), R : (A > (A > $o))]: ((![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ls)) => (R x x))) => (('const/list/LIST_REL' A A) R ls ls)))).
tt('thm/list/EVERY2_THM_0', ax, ![B : $t, A : $t]: (![P : (A > (B > $o)), ys : ('type/list/list' B)]: ((('const/list/LIST_REL' A B) P ('const/list/NIL' A) ys) = (ys = ('const/list/NIL' B))))).
tt('thm/list/EVERY2_THM_1', ax, ![D : $t, C : $t]: (![P : (C > (D > $o)), yys : ('type/list/list' D), x : C, xs : ('type/list/list' C)]: ((('const/list/LIST_REL' C D) P (('const/list/CONS' C) x xs) yys) = (?[y : D, ys : ('type/list/list' D)]: ((yys = (('const/list/CONS' D) y ys)) & ((P x y) & (('const/list/LIST_REL' C D) P xs ys))))))).
tt('thm/list/EVERY2_THM_2', ax, ![E : $t, F : $t]: (![P : (E > (F > $o)), xs : ('type/list/list' E)]: ((('const/list/LIST_REL' E F) P xs ('const/list/NIL' F)) = (xs = ('const/list/NIL' E))))).
tt('thm/list/EVERY2_THM_e3', ax, ![H : $t, G : $t]: (![P : (G > (H > $o)), xxs : ('type/list/list' G), y : H, ys : ('type/list/list' H)]: ((('const/list/LIST_REL' G H) P xxs (('const/list/CONS' H) y ys)) = (?[x : G, xs : ('type/list/list' G)]: ((xxs = (('const/list/CONS' G) x xs)) & ((P x y) & (('const/list/LIST_REL' G H) P xs ys))))))).
tt('thm/list/LIST_REL_trans_', ax, ![A : $t]: (![R : (A > (A > $o)), l1 : ('type/list/list' A), l2 : ('type/list/list' A), l3 : ('type/list/list' A)]: (((![n : 'type/num/num']: ((('const/prim_rec/<' n (('const/list/LENGTH' A) l1)) & ((R (('const/list/EL' A) n l1) (('const/list/EL' A) n l2)) & (R (('const/list/EL' A) n l2) (('const/list/EL' A) n l3)))) => (R (('const/list/EL' A) n l1) (('const/list/EL' A) n l3)))) & ((('const/list/LIST_REL' A A) R l1 l2) & (('const/list/LIST_REL' A A) R l2 l3))) => (('const/list/LIST_REL' A A) R l1 l3)))).
tt('thm/list/SWAP_REVERSE_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((l1 = (('const/list/REVERSE' A) l2)) = (l2 = (('const/list/REVERSE' A) l1))))).
tt('thm/list/SWAP_REVERSE_SYM_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/REVERSE' A) l1) = l2) = (l1 = (('const/list/REVERSE' A) l2))))).
tt('thm/list/BIGUNION_IMAGE_set_SUBSET_', ax, ![A : $t, B : $t]: (![s : (A > $o), ls : ('type/list/list' B), f : (B > (A > $o))]: ((('const/pred_set/SUBSET' A) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' B (A > $o)) f (('const/list/LIST_TO_SET' B) ls))) s) = (![x : B]: ((('const/bool/IN' B) x (('const/list/LIST_TO_SET' B) ls)) => (('const/pred_set/SUBSET' A) (f x) s)))))).
tt('thm/list/IMAGE_EL_count_LENGTH_', ax, ![A : $t, B : $t]: (![f : (A > B), ls : ('type/list/list' A)]: ((('const/pred_set/IMAGE' 'type/num/num' B) (^[n : 'type/num/num']: (f (('const/list/EL' A) n ls))) ('const/pred_set/count' (('const/list/LENGTH' A) ls))) = (('const/pred_set/IMAGE' A B) f (('const/list/LIST_TO_SET' A) ls))))).
tt('thm/list/GENLIST_EL_MAP_', ax, ![A : $t, B : $t]: (![f : (A > B), ls : ('type/list/list' A)]: ((('const/list/GENLIST' B) (^[n : 'type/num/num']: (f (('const/list/EL' A) n ls))) (('const/list/LENGTH' A) ls)) = (('const/list/MAP' A B) f ls)))).
tt('thm/list/LENGTH_FILTER_LEQ_MONO_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o)]: ((![x : A]: ((P x) => (Q x))) => (![ls : ('type/list/list' A)]: ('const/arithmetic/<=' (('const/list/LENGTH' A) (('const/list/FILTER' A) P ls)) (('const/list/LENGTH' A) (('const/list/FILTER' A) Q ls))))))).
tt('thm/list/LIST_EQ_MAP_PAIR_', ax, ![A : $t, B : $t]: (![l1 : ('type/list/list' ('type/pair/prod' A B)), l2 : ('type/list/list' ('type/pair/prod' A B))]: ((((('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) l1) = (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) l2)) & ((('const/list/MAP' ('type/pair/prod' A B) B) ('const/pair/SND' A B) l1) = (('const/list/MAP' ('type/pair/prod' A B) B) ('const/pair/SND' A B) l2))) => (l1 = l2)))).
tt('thm/list/TAKE_SUM_', 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/TAKE' A) ('const/arithmetic/+' n m) l) = (('const/list/APPEND' A) (('const/list/TAKE' A) n l) (('const/list/TAKE' A) m (('const/list/DROP' A) n l))))))).
tt('thm/list/ALL_DISTINCT_FILTER_EL_IMP_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A), n1 : 'type/num/num', n2 : 'type/num/num']: (((('const/list/ALL_DISTINCT' A) (('const/list/FILTER' A) P l)) & (('const/prim_rec/<' n1 (('const/list/LENGTH' A) l)) & (('const/prim_rec/<' n2 (('const/list/LENGTH' A) l)) & ((P (('const/list/EL' A) n1 l)) & ((('const/list/EL' A) n1 l) = (('const/list/EL' A) n2 l)))))) => (n1 = n2)))).
tt('thm/list/FLAT_EQ_NIL_', ax, ![A : $t]: (![ls : ('type/list/list' ('type/list/list' A))]: (((('const/list/FLAT' A) ls) = ('const/list/NIL' A)) = (('const/list/EVERY' ('type/list/list' A)) (($equals ('type/list/list' A)) ('const/list/NIL' A)) ls)))).
tt('thm/list/ALL_DISTINCT_MAP_INJ_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' A), f : (A > B)]: (((![x : A, y : A]: (((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ls)) & ((('const/bool/IN' A) y (('const/list/LIST_TO_SET' A) ls)) & ((f x) = (f y)))) => (x = y))) & (('const/list/ALL_DISTINCT' A) ls)) => (('const/list/ALL_DISTINCT' B) (('const/list/MAP' A B) f ls))))).
tt('thm/list/LENGTH_o_REVERSE_0', ax, ![A : $t]: ((('const/combin/o' ('type/list/list' A) 'type/num/num' ('type/list/list' A)) ('const/list/LENGTH' A) ('const/list/REVERSE' A)) = ('const/list/LENGTH' A))).
tt('thm/list/LENGTH_o_REVERSE_e1', ax, ![B : $t, C : $t]: (![f : (B > ('type/list/list' C))]: ((('const/combin/o' B 'type/num/num' ('type/list/list' C)) ('const/list/LENGTH' C) (('const/combin/o' B ('type/list/list' C) ('type/list/list' C)) ('const/list/REVERSE' C) f)) = (('const/combin/o' B 'type/num/num' ('type/list/list' C)) ('const/list/LENGTH' C) f)))).
tt('thm/list/REVERSE_o_REVERSE_', ax, ![A : $t, B : $t]: (![f : (A > ('type/list/list' B))]: ((('const/combin/o' A ('type/list/list' B) ('type/list/list' B)) ('const/list/REVERSE' B) (('const/combin/o' A ('type/list/list' B) ('type/list/list' B)) ('const/list/REVERSE' B) f)) = f))).
tt('thm/list/GENLIST_PLUS_APPEND_', ax, (![n2 : 'type/num/num', n1 : 'type/num/num', a : 'type/num/num']: ((('const/list/APPEND' 'type/num/num') (('const/list/GENLIST' 'type/num/num') ('const/arithmetic/+' a) n1) (('const/list/GENLIST' 'type/num/num') ('const/arithmetic/+' ('const/arithmetic/+' n1 a)) n2)) = (('const/list/GENLIST' 'type/num/num') ('const/arithmetic/+' a) ('const/arithmetic/+' n1 n2))))).
tt('thm/list/LIST_TO_SET_GENLIST_', ax, ![A : $t]: (![f : ('type/num/num' > A), n : 'type/num/num']: ((('const/list/LIST_TO_SET' A) (('const/list/GENLIST' A) f n)) = (('const/pred_set/IMAGE' 'type/num/num' A) f ('const/pred_set/count' n))))).
tt('thm/list/MEM_ZIP_MEM_MAP_', ax, ![A : $t, B : $t]: (![ps : ('type/pair/prod' ('type/list/list' A) ('type/list/list' B)), p : ('type/pair/prod' A B)]: ((((('const/list/LENGTH' A) (('const/pair/FST' ('type/list/list' A) ('type/list/list' B)) ps)) = (('const/list/LENGTH' B) (('const/pair/SND' ('type/list/list' A) ('type/list/list' B)) ps))) & (('const/bool/IN' ('type/pair/prod' A B)) p (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) (('const/list/ZIP' A B) ps)))) => ((('const/bool/IN' A) (('const/pair/FST' A B) p) (('const/list/LIST_TO_SET' A) (('const/pair/FST' ('type/list/list' A) ('type/list/list' B)) ps))) & (('const/bool/IN' B) (('const/pair/SND' A B) p) (('const/list/LIST_TO_SET' B) (('const/pair/SND' ('type/list/list' A) ('type/list/list' B)) ps))))))).
tt('thm/list/DISJOINT_GENLIST_PLUS_', ax, (![x : ('type/num/num' > $o), n : 'type/num/num', b : 'type/num/num', a : 'type/num/num']: ((('const/pred_set/DISJOINT' 'type/num/num') x (('const/list/LIST_TO_SET' 'type/num/num') (('const/list/GENLIST' 'type/num/num') ('const/arithmetic/+' n) ('const/arithmetic/+' a b)))) => ((('const/pred_set/DISJOINT' 'type/num/num') x (('const/list/LIST_TO_SET' 'type/num/num') (('const/list/GENLIST' 'type/num/num') ('const/arithmetic/+' n) a))) & (('const/pred_set/DISJOINT' 'type/num/num') x (('const/list/LIST_TO_SET' 'type/num/num') (('const/list/GENLIST' 'type/num/num') ('const/arithmetic/+' ('const/arithmetic/+' n a)) b))))))).
tt('thm/list/EVERY2_MAP_0', ax, ![B : $t, C : $t, A : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' C), f : (C > A), P : (A > (B > $o))]: ((('const/list/LIST_REL' A B) P (('const/list/MAP' C A) f l1) l2) = (('const/list/LIST_REL' C B) (^[x : C, y : B]: (P (f x) y)) l1 l2)))).
tt('thm/list/EVERY2_MAP_e1', ax, ![B : $t, C : $t, D : $t]: (![l2 : ('type/list/list' B), l1 : ('type/list/list' C), g : (B > D), Q : (C > (D > $o))]: ((('const/list/LIST_REL' C D) Q l1 (('const/list/MAP' B D) g l2)) = (('const/list/LIST_REL' C B) (^[x : C, y : B]: (Q x (g y))) l1 l2)))).
tt('thm/list/exists_list_GENLIST_', ax, ![A : $t]: (![P : (('type/list/list' A) > $o)]: ((?[ls : ('type/list/list' A)]: (P ls)) = (?[n : 'type/num/num', f : ('type/num/num' > A)]: (P (('const/list/GENLIST' A) f n)))))).
tt('thm/list/EVERY_MEM_MONO_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o), l : ('type/list/list' A)]: (((![x : A]: (((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l)) & (P x)) => (Q x))) & (('const/list/EVERY' A) P l)) => (('const/list/EVERY' A) Q l)))).
tt('thm/list/EVERY2_MEM_MONO_', ax, ![B : $t, A : $t]: (![P : (A > (B > $o)), Q : (A > (B > $o)), l1 : ('type/list/list' A), l2 : ('type/list/list' B)]: (((![x : ('type/pair/prod' A B)]: (((('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)) l1 l2)))) & (('const/pair/UNCURRY' A B $o) P x)) => (('const/pair/UNCURRY' A B $o) Q x))) & (('const/list/LIST_REL' A B) P l1 l2)) => (('const/list/LIST_REL' A B) Q l1 l2)))).
tt('thm/list/mem_exists_set_', ax, ![A : $t, B : $t]: (![x : A, y : B, l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) l)) => (?[z : ('type/pair/prod' A B)]: ((x = (('const/pair/FST' A B) z)) & (('const/bool/IN' ('type/pair/prod' A B)) z (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) l))))))).
tt('thm/list/every_zip_snd_', ax, ![B : $t, A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B), P : (B > $o)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => ((('const/list/EVERY' ('type/pair/prod' A B)) (^[x : ('type/pair/prod' A B)]: (P (('const/pair/SND' A B) x))) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/EVERY' B) P l2))))).
tt('thm/list/every_zip_fst_', ax, ![A : $t, B : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' B), P : (A > $o)]: (((('const/list/LENGTH' A) l1) = (('const/list/LENGTH' B) l2)) => ((('const/list/EVERY' ('type/pair/prod' A B)) (^[x : ('type/pair/prod' A B)]: (P (('const/pair/FST' A B) x))) (('const/list/ZIP' A B) (('const/pair/,' ('type/list/list' A) ('type/list/list' B)) l1 l2))) = (('const/list/EVERY' A) P l1))))).
tt('thm/list/el_append3_', ax, ![A : $t]: (![l1 : ('type/list/list' A), x : A, l2 : ('type/list/list' A)]: ((('const/list/EL' A) (('const/list/LENGTH' A) l1) (('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) x ('const/list/NIL' A))) l2)) = x))).
tt('thm/list/lupdate_append_', ax, ![A : $t]: (![x : A, 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/LUPDATE' A) x n (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/list/LUPDATE' A) x n l1) l2))))).
tt('thm/list/lupdate_append2_', ax, ![A : $t, B : $t]: (![v : A, l1 : ('type/list/list' A), x : A, l2 : ('type/list/list' A), l3 : B]: ((('const/list/LUPDATE' A) v (('const/list/LENGTH' A) l1) (('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) x ('const/list/NIL' A))) l2)) = (('const/list/APPEND' A) (('const/list/APPEND' A) l1 (('const/list/CONS' A) v ('const/list/NIL' A))) l2)))).
tt('thm/list/LAST_REVERSE_', ax, ![A : $t]: (![ls : ('type/list/list' A)]: ((~ (ls = ('const/list/NIL' A))) => ((('const/list/LAST' A) (('const/list/REVERSE' A) ls)) = (('const/list/HD' A) ls))))).
tt('thm/list/dropWhile_def_0', def, ![A : $t]: (![P : (A > $o)]: ((('const/list/dropWhile' A) P ('const/list/NIL' A)) = ('const/list/NIL' A)))).
tt('thm/list/dropWhile_def_e1', def, ![A : $t]: (![P : (A > $o), h : A, t : ('type/list/list' A)]: ((('const/list/dropWhile' A) P (('const/list/CONS' A) h t)) = (('const/bool/COND' ('type/list/list' A)) (P h) (('const/list/dropWhile' A) P t) (('const/list/CONS' A) h t))))).
tt('thm/list/dropWhile_splitAtPki_', ax, ![A : $t]: (![P : (A > $o)]: ((('const/list/dropWhile' A) P) = (('const/list/splitAtPki' ('type/list/list' A) A) (('const/combin/C' A 'type/num/num' $o) (('const/combin/o' A ('type/num/num' > $o) $o) ('const/combin/K' $o 'type/num/num') (('const/combin/o' A $o $o) $not P))) (('const/combin/K' (('type/list/list' A) > ('type/list/list' A)) ('type/list/list' A)) ('const/combin/I' ('type/list/list' A))))))).
tt('thm/list/dropWhile_eq_nil_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A)]: (((('const/list/dropWhile' A) P ls) = ('const/list/NIL' A)) = (('const/list/EVERY' A) P ls)))).
tt('thm/list/MEM_dropWhile_IMP_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A), x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/dropWhile' A) P ls))) => (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ls))))).
tt('thm/list/HD_dropWhile_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A)]: ((('const/list/EXISTS' A) (('const/combin/o' A $o $o) $not P) ls) => (~ (P (('const/list/HD' A) (('const/list/dropWhile' A) P ls))))))).
tt('thm/list/LENGTH_dropWhile_LESS_EQ_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A)]: ('const/arithmetic/<=' (('const/list/LENGTH' A) (('const/list/dropWhile' A) P ls)) (('const/list/LENGTH' A) ls)))).
tt('thm/list/dropWhile_APPEND_EVERY_', ax, ![A : $t]: (![P : (A > $o), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/EVERY' A) P l1) => ((('const/list/dropWhile' A) P (('const/list/APPEND' A) l1 l2)) = (('const/list/dropWhile' A) P l2))))).
tt('thm/list/dropWhile_APPEND_EXISTS_', ax, ![A : $t]: (![P : (A > $o), l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: ((('const/list/EXISTS' A) (('const/combin/o' A $o $o) $not P) l1) => ((('const/list/dropWhile' A) P (('const/list/APPEND' A) l1 l2)) = (('const/list/APPEND' A) (('const/list/dropWhile' A) P l1) l2))))).
tt('thm/list/EL_LENGTH_dropWhile_REVERSE_', ax, ![A : $t]: (![P : (A > $o), ls : ('type/list/list' A), k : 'type/num/num']: ((('const/arithmetic/<=' (('const/list/LENGTH' A) (('const/list/dropWhile' A) P (('const/list/REVERSE' A) ls))) k) & ('const/prim_rec/<' k (('const/list/LENGTH' A) ls))) => (P (('const/list/EL' A) k ls))))).
tt('thm/list/LAST_compute_0', ax, ![A : $t]: (![x : A]: ((('const/list/LAST' A) (('const/list/CONS' A) x ('const/list/NIL' A))) = x))).
tt('thm/list/LAST_compute_e1', ax, ![B : $t]: (![h1 : B, h2 : B, t : ('type/list/list' B)]: ((('const/list/LAST' B) (('const/list/CONS' B) h1 (('const/list/CONS' B) h2 t))) = (('const/list/LAST' B) (('const/list/CONS' B) h2 t))))).
tt('thm/list/TAKE_compute_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/TAKE' A) 'const/num/0' l) = ('const/list/NIL' A)))).
tt('thm/list/TAKE_compute_1', ax, ![B : $t]: (![n : 'type/num/num']: ((('const/list/TAKE' B) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/list/NIL' B)) = ('const/list/NIL' B)))).
tt('thm/list/TAKE_compute_2', ax, ![B : $t]: (![n : 'type/num/num']: ((('const/list/TAKE' B) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) ('const/list/NIL' B)) = ('const/list/NIL' B)))).
tt('thm/list/TAKE_compute_3', ax, ![C : $t]: (![n : 'type/num/num', h : C, t : ('type/list/list' C)]: ((('const/list/TAKE' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/CONS' C) h t)) = (('const/list/CONS' C) h (('const/list/TAKE' C) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) t))))).
tt('thm/list/TAKE_compute_e4', ax, ![C : $t]: (![n : 'type/num/num', h : C, t : ('type/list/list' C)]: ((('const/list/TAKE' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) (('const/list/CONS' C) h t)) = (('const/list/CONS' C) h (('const/list/TAKE' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) t))))).
tt('thm/list/DROP_compute_0', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/DROP' A) 'const/num/0' l) = l))).
tt('thm/list/DROP_compute_1', ax, ![B : $t]: (![n : 'type/num/num']: ((('const/list/DROP' B) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/list/NIL' B)) = ('const/list/NIL' B)))).
tt('thm/list/DROP_compute_2', ax, ![B : $t]: (![n : 'type/num/num']: ((('const/list/DROP' B) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) ('const/list/NIL' B)) = ('const/list/NIL' B)))).
tt('thm/list/DROP_compute_3', ax, ![C : $t]: (![n : 'type/num/num', h : C, t : ('type/list/list' C)]: ((('const/list/DROP' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) (('const/list/CONS' C) h t)) = (('const/list/DROP' C) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) t)))).
tt('thm/list/DROP_compute_e4', ax, ![C : $t]: (![n : 'type/num/num', h : C, t : ('type/list/list' C)]: ((('const/list/DROP' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) (('const/list/CONS' C) h t)) = (('const/list/DROP' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) t)))).
