tt('const/pred_set/BIGINTER', ty, ![A : $t]: (((A > $o) > $o) > (A > $o))).
tt('const/pred_set/BIGUNION', ty, ![A : $t]: (((A > $o) > $o) > (A > $o))).
tt('const/pred_set/BIJ', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > ((B > $o) > $o)))).
tt('const/pred_set/CARD', ty, ![A : $t]: ((A > $o) > 'type/num/num')).
tt('const/pred_set/CHOICE', ty, ![A : $t]: ((A > $o) > A)).
tt('const/pred_set/COMPL', ty, ![A : $t]: ((A > $o) > (A > $o))).
tt('const/pred_set/CROSS', ty, ![A : $t, B : $t]: ((A > $o) > ((B > $o) > (('type/pair/prod' A B) > $o)))).
tt('const/pred_set/DELETE', ty, ![A : $t]: ((A > $o) > (A > (A > $o)))).
tt('const/pred_set/DIFF', ty, ![A : $t]: ((A > $o) > ((A > $o) > (A > $o)))).
tt('const/pred_set/DISJOINT', ty, ![A : $t]: ((A > $o) > ((A > $o) > $o))).
tt('const/pred_set/EMPTY', ty, ![A : $t]: (A > $o)).
tt('const/pred_set/FINITE', ty, ![A : $t]: ((A > $o) > $o)).
tt('const/pred_set/GSPEC', ty, ![A : $t, B : $t]: ((B > ('type/pair/prod' A $o)) > (A > $o))).
tt('const/pred_set/IMAGE', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > (B > $o)))).
tt('const/pred_set/INJ', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > ((B > $o) > $o)))).
tt('const/pred_set/INSERT', ty, ![A : $t]: (A > ((A > $o) > (A > $o)))).
tt('const/pred_set/INTER', ty, ![A : $t]: ((A > $o) > ((A > $o) > (A > $o)))).
tt('const/pred_set/ITSET', ty, ![A : $t, B : $t]: ((A > (B > B)) > ((A > $o) > (B > B)))).
tt('const/pred_set/ITSET_tupled', ty, ![A : $t, B : $t]: ((A > (B > B)) > (('type/pair/prod' (A > $o) B) > B))).
tt('const/pred_set/LINV', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > (B > A)))).
tt('const/pred_set/MAX_SET', ty, (('type/num/num' > $o) > 'type/num/num')).
tt('const/pred_set/MIN_SET', ty, (('type/num/num' > $o) > 'type/num/num')).
tt('const/pred_set/POW', ty, ![A : $t]: ((A > $o) > ((A > $o) > $o))).
tt('const/pred_set/PROD_IMAGE', ty, ![A : $t]: ((A > 'type/num/num') > ((A > $o) > 'type/num/num'))).
tt('const/pred_set/PROD_SET', ty, (('type/num/num' > $o) > 'type/num/num')).
tt('const/pred_set/PSUBSET', ty, ![A : $t]: ((A > $o) > ((A > $o) > $o))).
tt('const/pred_set/REL_RESTRICT', ty, ![A : $t]: ((A > (A > $o)) > ((A > $o) > (A > (A > $o))))).
tt('const/pred_set/REST', ty, ![A : $t]: ((A > $o) > (A > $o))).
tt('const/pred_set/RINV', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > (B > A)))).
tt('const/pred_set/SING', ty, ![A : $t]: ((A > $o) > $o)).
tt('const/pred_set/SUBSET', ty, ![A : $t]: ((A > $o) > ((A > $o) > $o))).
tt('const/pred_set/SUM_IMAGE', ty, ![A : $t]: ((A > 'type/num/num') > ((A > $o) > 'type/num/num'))).
tt('const/pred_set/SUM_SET', ty, (('type/num/num' > $o) > 'type/num/num')).
tt('const/pred_set/SURJ', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > ((B > $o) > $o)))).
tt('const/pred_set/UNION', ty, ![A : $t]: ((A > $o) > ((A > $o) > (A > $o)))).
tt('const/pred_set/UNIV', ty, ![A : $t]: (A > $o)).
tt('const/pred_set/chooser', ty, ![A : $t]: ((A > $o) > ('type/num/num' > A))).
tt('const/pred_set/count', ty, ('type/num/num' > ('type/num/num' > $o))).
tt('const/pred_set/countable', ty, ![A : $t]: ((A > $o) > $o)).
tt('const/pred_set/equiv_on', ty, ![A : $t]: ((A > (A > $o)) > ((A > $o) > $o))).
tt('const/pred_set/num_to_pair', ty, ('type/num/num' > ('type/pair/prod' 'type/num/num' 'type/num/num'))).
tt('const/pred_set/pair_to_num', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/pred_set/pairwise', ty, ![A : $t]: ((A > (A > $o)) > ((A > $o) > $o))).
tt('const/pred_set/partition', ty, ![A : $t]: ((A > (A > $o)) > ((A > $o) > ((A > $o) > $o)))).
tt('thm/pred_set/SPECIFICATION_', ax, ![A : $t]: (![P : (A > $o), x : A]: ((('const/bool/IN' A) x P) = (P x)))).
tt('thm/pred_set/IN_ABS_', ax, ![A : $t]: (![x : A, P : (A > $o)]: ((('const/bool/IN' A) x (^[x0 : A]: (P x0))) = (P x)))).
tt('thm/pred_set/ABS_applied_', ax, $true).
tt('thm/pred_set/EXTENSION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((s = t) = (![x : A]: ((('const/bool/IN' A) x s) = (('const/bool/IN' A) x t)))))).
tt('thm/pred_set/NOT_EQUAL_SETS_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((~ (s = t)) = (?[x : A]: ((('const/bool/IN' A) x t) = (~ (('const/bool/IN' A) x s))))))).
tt('thm/pred_set/NUM_SET_WOP_', ax, (![s : ('type/num/num' > $o)]: ((?[n : 'type/num/num']: (('const/bool/IN' 'type/num/num') n s)) = (?[n : 'type/num/num']: ((('const/bool/IN' 'type/num/num') n s) & (![m : 'type/num/num']: ((('const/bool/IN' 'type/num/num') m s) => ('const/arithmetic/<=' n m)))))))).
tt('thm/pred_set/GSPECIFICATION_', def, ![B : $t, A : $t]: (![f : (B > ('type/pair/prod' A $o)), v : A]: ((('const/bool/IN' A) v (('const/pred_set/GSPEC' A B) f)) = (?[x : B]: ((('const/pair/,' A $o) v $true) = (f x)))))).
tt('thm/pred_set/GSPECIFICATION_applied_', ax, ![B : $t, A : $t]: (![f : (B > ('type/pair/prod' A $o)), v : A]: ((('const/pred_set/GSPEC' A B) f v) = (?[x : B]: ((('const/pair/,' A $o) v $true) = (f x)))))).
tt('thm/pred_set/SET_MINIMUM_', ax, ![A : $t]: (![s : (A > $o), M : (A > 'type/num/num')]: ((?[x : A]: (('const/bool/IN' A) x s)) = (?[x : A]: ((('const/bool/IN' A) x s) & (![y : A]: ((('const/bool/IN' A) y s) => ('const/arithmetic/<=' (M x) (M y))))))))).
tt('thm/pred_set/EMPTY_DEF_', def, ![A : $t]: (('const/pred_set/EMPTY' A) = (^[x : A]: $false))).
tt('thm/pred_set/NOT_IN_EMPTY_', ax, ![A : $t]: (![x : A]: (~ (('const/bool/IN' A) x ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/MEMBER_NOT_EMPTY_', ax, ![A : $t]: (![s : (A > $o)]: ((?[x : A]: (('const/bool/IN' A) x s)) = (~ (s = ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/EMPTY_applied_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/EMPTY' A) x) = $false))).
tt('thm/pred_set/UNIV_DEF_', def, ![A : $t]: (('const/pred_set/UNIV' A) = (^[x : A]: $true))).
tt('thm/pred_set/IN_UNIV_', ax, ![A : $t]: (![x : A]: (('const/bool/IN' A) x ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/UNIV_NOT_EMPTY_', ax, ![A : $t]: (~ (('const/pred_set/UNIV' A) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/EMPTY_NOT_UNIV_', ax, ![A : $t]: (~ (('const/pred_set/EMPTY' A) = ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/EQ_UNIV_', ax, ![A : $t]: (![s : (A > $o)]: ((![x : A]: (('const/bool/IN' A) x s)) = (s = ('const/pred_set/UNIV' A))))).
tt('thm/pred_set/SUBSET_DEF_', def, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) s t) = (![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' A) x t)))))).
tt('thm/pred_set/SUBSET_TRANS_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/pred_set/SUBSET' A) s t) & (('const/pred_set/SUBSET' A) t u)) => (('const/pred_set/SUBSET' A) s u)))).
tt('thm/pred_set/SUBSET_REFL_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/SUBSET' A) s s))).
tt('thm/pred_set/SUBSET_ANTISYM_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/SUBSET' A) s t) & (('const/pred_set/SUBSET' A) t s)) => (s = t)))).
tt('thm/pred_set/EMPTY_SUBSET_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/SUBSET' A) ('const/pred_set/EMPTY' A) s))).
tt('thm/pred_set/SUBSET_EMPTY_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/SUBSET' A) s ('const/pred_set/EMPTY' A)) = (s = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/SUBSET_UNIV_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/SUBSET' A) s ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/UNIV_SUBSET_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/SUBSET' A) ('const/pred_set/UNIV' A) s) = (s = ('const/pred_set/UNIV' A))))).
tt('thm/pred_set/PSUBSET_DEF_', def, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/PSUBSET' A) s t) = ((('const/pred_set/SUBSET' A) s t) & (~ (s = t)))))).
tt('thm/pred_set/PSUBSET_TRANS_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/pred_set/PSUBSET' A) s t) & (('const/pred_set/PSUBSET' A) t u)) => (('const/pred_set/PSUBSET' A) s u)))).
tt('thm/pred_set/PSUBSET_IRREFL_', ax, ![A : $t]: (![s : (A > $o)]: (~ (('const/pred_set/PSUBSET' A) s s)))).
tt('thm/pred_set/NOT_PSUBSET_EMPTY_', ax, ![A : $t]: (![s : (A > $o)]: (~ (('const/pred_set/PSUBSET' A) s ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/NOT_UNIV_PSUBSET_', ax, ![A : $t]: (![s : (A > $o)]: (~ (('const/pred_set/PSUBSET' A) ('const/pred_set/UNIV' A) s)))).
tt('thm/pred_set/PSUBSET_UNIV_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/PSUBSET' A) s ('const/pred_set/UNIV' A)) = (?[x : A]: (~ (('const/bool/IN' A) x s)))))).
tt('thm/pred_set/UNION_DEF_', def, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/UNION' A) s t) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x s) | (('const/bool/IN' A) x t)))))))).
tt('thm/pred_set/IN_UNION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/bool/IN' A) x (('const/pred_set/UNION' A) s t)) = ((('const/bool/IN' A) x s) | (('const/bool/IN' A) x t))))).
tt('thm/pred_set/UNION_applied_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/UNION' A) s t x) = ((('const/bool/IN' A) x s) | (('const/bool/IN' A) x t))))).
tt('thm/pred_set/UNION_ASSOC_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/UNION' A) s (('const/pred_set/UNION' A) t u)) = (('const/pred_set/UNION' A) (('const/pred_set/UNION' A) s t) u)))).
tt('thm/pred_set/UNION_IDEMPOT_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/UNION' A) s s) = s))).
tt('thm/pred_set/UNION_COMM_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/UNION' A) s t) = (('const/pred_set/UNION' A) t s)))).
tt('thm/pred_set/SUBSET_UNION_0', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (('const/pred_set/SUBSET' A) s (('const/pred_set/UNION' A) s t)))).
tt('thm/pred_set/SUBSET_UNION_e1', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (('const/pred_set/SUBSET' A) s (('const/pred_set/UNION' A) t s)))).
tt('thm/pred_set/UNION_SUBSET_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/SUBSET' A) (('const/pred_set/UNION' A) s t) u) = ((('const/pred_set/SUBSET' A) s u) & (('const/pred_set/SUBSET' A) t u))))).
tt('thm/pred_set/SUBSET_UNION_ABSORPTION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) s t) = ((('const/pred_set/UNION' A) s t) = t)))).
tt('thm/pred_set/UNION_EMPTY_0', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/UNION' A) ('const/pred_set/EMPTY' A) s) = s))).
tt('thm/pred_set/UNION_EMPTY_e1', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/UNION' A) s ('const/pred_set/EMPTY' A)) = s))).
tt('thm/pred_set/UNION_UNIV_0', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/UNION' A) ('const/pred_set/UNIV' A) s) = ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/UNION_UNIV_e1', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/UNION' A) s ('const/pred_set/UNIV' A)) = ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/EMPTY_UNION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/UNION' A) s t) = ('const/pred_set/EMPTY' A)) = ((s = ('const/pred_set/EMPTY' A)) & (t = ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/INTER_DEF_', def, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/INTER' A) s t) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x s) & (('const/bool/IN' A) x t)))))))).
tt('thm/pred_set/IN_INTER_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/bool/IN' A) x (('const/pred_set/INTER' A) s t)) = ((('const/bool/IN' A) x s) & (('const/bool/IN' A) x t))))).
tt('thm/pred_set/INTER_applied_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/INTER' A) s t x) = ((('const/bool/IN' A) x s) & (('const/bool/IN' A) x t))))).
tt('thm/pred_set/INTER_ASSOC_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/INTER' A) s (('const/pred_set/INTER' A) t u)) = (('const/pred_set/INTER' A) (('const/pred_set/INTER' A) s t) u)))).
tt('thm/pred_set/INTER_IDEMPOT_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/INTER' A) s s) = s))).
tt('thm/pred_set/INTER_COMM_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/INTER' A) s t) = (('const/pred_set/INTER' A) t s)))).
tt('thm/pred_set/INTER_SUBSET_0', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (('const/pred_set/SUBSET' A) (('const/pred_set/INTER' A) s t) s))).
tt('thm/pred_set/INTER_SUBSET_e1', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (('const/pred_set/SUBSET' A) (('const/pred_set/INTER' A) t s) s))).
tt('thm/pred_set/SUBSET_INTER_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/SUBSET' A) s (('const/pred_set/INTER' A) t u)) = ((('const/pred_set/SUBSET' A) s t) & (('const/pred_set/SUBSET' A) s u))))).
tt('thm/pred_set/SUBSET_INTER_ABSORPTION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) s t) = ((('const/pred_set/INTER' A) s t) = s)))).
tt('thm/pred_set/INTER_EMPTY_0', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/INTER' A) ('const/pred_set/EMPTY' A) s) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/INTER_EMPTY_e1', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/INTER' A) s ('const/pred_set/EMPTY' A)) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/INTER_UNIV_0', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/INTER' A) ('const/pred_set/UNIV' A) s) = s))).
tt('thm/pred_set/INTER_UNIV_e1', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/INTER' A) s ('const/pred_set/UNIV' A)) = s))).
tt('thm/pred_set/UNION_OVER_INTER_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/INTER' A) s (('const/pred_set/UNION' A) t u)) = (('const/pred_set/UNION' A) (('const/pred_set/INTER' A) s t) (('const/pred_set/INTER' A) s u))))).
tt('thm/pred_set/INTER_OVER_UNION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/UNION' A) s (('const/pred_set/INTER' A) t u)) = (('const/pred_set/INTER' A) (('const/pred_set/UNION' A) s t) (('const/pred_set/UNION' A) s u))))).
tt('thm/pred_set/DISJOINT_DEF_', def, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) s t) = ((('const/pred_set/INTER' A) s t) = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/IN_DISJOINT_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) s t) = (~ (?[x : A]: ((('const/bool/IN' A) x s) & (('const/bool/IN' A) x t))))))).
tt('thm/pred_set/DISJOINT_SYM_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) s t) = (('const/pred_set/DISJOINT' A) t s)))).
tt('thm/pred_set/DISJOINT_EMPTY_0', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/DISJOINT' A) ('const/pred_set/EMPTY' A) s))).
tt('thm/pred_set/DISJOINT_EMPTY_e1', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/DISJOINT' A) s ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/DISJOINT_EMPTY_REFL_', ax, ![A : $t]: (![s : (A > $o)]: ((s = ('const/pred_set/EMPTY' A)) = (('const/pred_set/DISJOINT' A) s s)))).
tt('thm/pred_set/DISJOINT_EMPTY_REFL_RWT_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/DISJOINT' A) s s) = (s = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/DISJOINT_UNION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: ((('const/pred_set/DISJOINT' A) (('const/pred_set/UNION' A) s t) u) = ((('const/pred_set/DISJOINT' A) s u) & (('const/pred_set/DISJOINT' A) t u))))).
tt('thm/pred_set/DISJOINT_UNION_BOTH_0', ax, ![A : $t]: (![u : (A > $o), t : (A > $o), s : (A > $o)]: ((('const/pred_set/DISJOINT' A) (('const/pred_set/UNION' A) s t) u) = ((('const/pred_set/DISJOINT' A) s u) & (('const/pred_set/DISJOINT' A) t u))))).
tt('thm/pred_set/DISJOINT_UNION_BOTH_e1', ax, ![A : $t]: (![u : (A > $o), t : (A > $o), s : (A > $o)]: ((('const/pred_set/DISJOINT' A) u (('const/pred_set/UNION' A) s t)) = ((('const/pred_set/DISJOINT' A) s u) & (('const/pred_set/DISJOINT' A) t u))))).
tt('thm/pred_set/DISJOINT_SUBSET_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/pred_set/DISJOINT' A) s t) & (('const/pred_set/SUBSET' A) u t)) => (('const/pred_set/DISJOINT' A) s u)))).
tt('thm/pred_set/DIFF_DEF_', def, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/DIFF' A) s t) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x s) & (~ (('const/bool/IN' A) x t))))))))).
tt('thm/pred_set/IN_DIFF_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/bool/IN' A) x (('const/pred_set/DIFF' A) s t)) = ((('const/bool/IN' A) x s) & (~ (('const/bool/IN' A) x t)))))).
tt('thm/pred_set/DIFF_applied_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/DIFF' A) s t x) = ((('const/bool/IN' A) x s) & (~ (('const/bool/IN' A) x t)))))).
tt('thm/pred_set/DIFF_EMPTY_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/DIFF' A) s ('const/pred_set/EMPTY' A)) = s))).
tt('thm/pred_set/EMPTY_DIFF_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/DIFF' A) ('const/pred_set/EMPTY' A) s) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/DIFF_UNIV_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/DIFF' A) s ('const/pred_set/UNIV' A)) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/DIFF_DIFF_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/DIFF' A) (('const/pred_set/DIFF' A) s t) t) = (('const/pred_set/DIFF' A) s t)))).
tt('thm/pred_set/DIFF_EQ_EMPTY_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/DIFF' A) s s) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/DIFF_SUBSET_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (('const/pred_set/SUBSET' A) (('const/pred_set/DIFF' A) s t) s))).
tt('thm/pred_set/UNION_DIFF_', ax, ![A : $t]: (![t : (A > $o), s : (A > $o)]: ((('const/pred_set/SUBSET' A) s t) => (((('const/pred_set/UNION' A) s (('const/pred_set/DIFF' A) t s)) = t) & ((('const/pred_set/UNION' A) (('const/pred_set/DIFF' A) t s) s) = t))))).
tt('thm/pred_set/DIFF_UNION_', ax, ![A : $t]: (![x : (A > $o), y : (A > $o), z : (A > $o)]: ((('const/pred_set/DIFF' A) x (('const/pred_set/UNION' A) y z)) = (('const/pred_set/DIFF' A) (('const/pred_set/DIFF' A) x y) z)))).
tt('thm/pred_set/DIFF_COMM_', ax, ![A : $t]: (![x : (A > $o), y : (A > $o), z : (A > $o)]: ((('const/pred_set/DIFF' A) (('const/pred_set/DIFF' A) x y) z) = (('const/pred_set/DIFF' A) (('const/pred_set/DIFF' A) x z) y)))).
tt('thm/pred_set/DIFF_SAME_UNION_0', ax, ![A : $t]: (![y : (A > $o), x : (A > $o)]: ((('const/pred_set/DIFF' A) (('const/pred_set/UNION' A) x y) x) = (('const/pred_set/DIFF' A) y x)))).
tt('thm/pred_set/DIFF_SAME_UNION_e1', ax, ![A : $t]: (![y : (A > $o), x : (A > $o)]: ((('const/pred_set/DIFF' A) (('const/pred_set/UNION' A) x y) y) = (('const/pred_set/DIFF' A) x y)))).
tt('thm/pred_set/INSERT_DEF_', def, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/INSERT' A) x s) = (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((y = x) | (('const/bool/IN' A) y s)))))))).
tt('thm/pred_set/IN_INSERT_', ax, ![A : $t]: (![x : A, y : A, s : (A > $o)]: ((('const/bool/IN' A) x (('const/pred_set/INSERT' A) y s)) = ((x = y) | (('const/bool/IN' A) x s))))).
tt('thm/pred_set/INSERT_applied_', ax, ![A : $t]: (![x : A, y : A, s : (A > $o)]: ((('const/pred_set/INSERT' A) y s x) = ((x = y) | (('const/bool/IN' A) x s))))).
tt('thm/pred_set/COMPONENT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: (('const/bool/IN' A) x (('const/pred_set/INSERT' A) x s)))).
tt('thm/pred_set/SET_CASES_', ax, ![A : $t]: (![s : (A > $o)]: ((s = ('const/pred_set/EMPTY' A)) | (?[x : A, t : (A > $o)]: ((s = (('const/pred_set/INSERT' A) x t)) & (~ (('const/bool/IN' A) x t))))))).
tt('thm/pred_set/DECOMPOSITION_', ax, ![A : $t]: (![s : (A > $o), x : A]: ((('const/bool/IN' A) x s) = (?[t : (A > $o)]: ((s = (('const/pred_set/INSERT' A) x t)) & (~ (('const/bool/IN' A) x t))))))).
tt('thm/pred_set/ABSORPTION_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/bool/IN' A) x s) = ((('const/pred_set/INSERT' A) x s) = s)))).
tt('thm/pred_set/ABSORPTION_RWT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/bool/IN' A) x s) => ((('const/pred_set/INSERT' A) x s) = s)))).
tt('thm/pred_set/INSERT_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/INSERT' A) x (('const/pred_set/INSERT' A) x s)) = (('const/pred_set/INSERT' A) x s)))).
tt('thm/pred_set/INSERT_COMM_', ax, ![A : $t]: (![x : A, y : A, s : (A > $o)]: ((('const/pred_set/INSERT' A) x (('const/pred_set/INSERT' A) y s)) = (('const/pred_set/INSERT' A) y (('const/pred_set/INSERT' A) x s))))).
tt('thm/pred_set/INSERT_UNIV_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/INSERT' A) x ('const/pred_set/UNIV' A)) = ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/NOT_INSERT_EMPTY_', ax, ![A : $t]: (![x : A, s : (A > $o)]: (~ ((('const/pred_set/INSERT' A) x s) = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/NOT_EMPTY_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: (~ (('const/pred_set/EMPTY' A) = (('const/pred_set/INSERT' A) x s))))).
tt('thm/pred_set/INSERT_UNION_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/UNION' A) (('const/pred_set/INSERT' A) x s) t) = (('const/bool/COND' (A > $o)) (('const/bool/IN' A) x t) (('const/pred_set/UNION' A) s t) (('const/pred_set/INSERT' A) x (('const/pred_set/UNION' A) s t)))))).
tt('thm/pred_set/INSERT_UNION_EQ_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/UNION' A) (('const/pred_set/INSERT' A) x s) t) = (('const/pred_set/INSERT' A) x (('const/pred_set/UNION' A) s t))))).
tt('thm/pred_set/INSERT_INTER_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/INTER' A) (('const/pred_set/INSERT' A) x s) t) = (('const/bool/COND' (A > $o)) (('const/bool/IN' A) x t) (('const/pred_set/INSERT' A) x (('const/pred_set/INTER' A) s t)) (('const/pred_set/INTER' A) s t))))).
tt('thm/pred_set/DISJOINT_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) (('const/pred_set/INSERT' A) x s) t) = ((('const/pred_set/DISJOINT' A) s t) & (~ (('const/bool/IN' A) x t)))))).
tt('thm/pred_set/DISJOINT_INSERT\'_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) t (('const/pred_set/INSERT' A) x s)) = ((('const/pred_set/DISJOINT' A) t s) & (~ (('const/bool/IN' A) x t)))))).
tt('thm/pred_set/INSERT_SUBSET_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) (('const/pred_set/INSERT' A) x s) t) = ((('const/bool/IN' A) x t) & (('const/pred_set/SUBSET' A) s t))))).
tt('thm/pred_set/SUBSET_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((~ (('const/bool/IN' A) x s)) => (![t : (A > $o)]: ((('const/pred_set/SUBSET' A) s (('const/pred_set/INSERT' A) x t)) = (('const/pred_set/SUBSET' A) s t)))))).
tt('thm/pred_set/INSERT_DIFF_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/DIFF' A) (('const/pred_set/INSERT' A) x s) t) = (('const/bool/COND' (A > $o)) (('const/bool/IN' A) x t) (('const/pred_set/DIFF' A) s t) (('const/pred_set/INSERT' A) x (('const/pred_set/DIFF' A) s t)))))).
tt('thm/pred_set/UNIV_BOOL_', ax, (('const/pred_set/UNIV' $o) = (('const/pred_set/INSERT' $o) $true (('const/pred_set/INSERT' $o) $false ('const/pred_set/EMPTY' $o))))).
tt('thm/pred_set/DELETE_DEF_', def, ![A : $t]: (![s : (A > $o), x : A]: ((('const/pred_set/DELETE' A) s x) = (('const/pred_set/DIFF' A) s (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/IN_DELETE_', ax, ![A : $t]: (![s : (A > $o), x : A, y : A]: ((('const/bool/IN' A) x (('const/pred_set/DELETE' A) s y)) = ((('const/bool/IN' A) x s) & (~ (x = y)))))).
tt('thm/pred_set/DELETE_applied_', ax, ![A : $t]: (![s : (A > $o), x : A, y : A]: ((('const/pred_set/DELETE' A) s y x) = ((('const/bool/IN' A) x s) & (~ (x = y)))))).
tt('thm/pred_set/DELETE_NON_ELEMENT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((~ (('const/bool/IN' A) x s)) = ((('const/pred_set/DELETE' A) s x) = s)))).
tt('thm/pred_set/DELETE_NON_ELEMENT_RWT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((~ (('const/bool/IN' A) x s)) => ((('const/pred_set/DELETE' A) s x) = s)))).
tt('thm/pred_set/IN_DELETE_EQ_', ax, ![A : $t]: (![s : (A > $o), x : A, 'x\'' : A]: (((('const/bool/IN' A) x s) = (('const/bool/IN' A) 'x\'' s)) = ((('const/bool/IN' A) x (('const/pred_set/DELETE' A) s 'x\'')) = (('const/bool/IN' A) 'x\'' (('const/pred_set/DELETE' A) s x)))))).
tt('thm/pred_set/EMPTY_DELETE_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/DELETE' A) ('const/pred_set/EMPTY' A) x) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/DELETE_DELETE_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/DELETE' A) (('const/pred_set/DELETE' A) s x) x) = (('const/pred_set/DELETE' A) s x)))).
tt('thm/pred_set/DELETE_COMM_', ax, ![A : $t]: (![x : A, y : A, s : (A > $o)]: ((('const/pred_set/DELETE' A) (('const/pred_set/DELETE' A) s x) y) = (('const/pred_set/DELETE' A) (('const/pred_set/DELETE' A) s y) x)))).
tt('thm/pred_set/DELETE_SUBSET_', ax, ![A : $t]: (![x : A, s : (A > $o)]: (('const/pred_set/SUBSET' A) (('const/pred_set/DELETE' A) s x) s))).
tt('thm/pred_set/SUBSET_DELETE_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) s (('const/pred_set/DELETE' A) t x)) = ((~ (('const/bool/IN' A) x s)) & (('const/pred_set/SUBSET' A) s t))))).
tt('thm/pred_set/SUBSET_INSERT_DELETE_', ax, ![A : $t]: (![x : A, s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) s (('const/pred_set/INSERT' A) x t)) = (('const/pred_set/SUBSET' A) (('const/pred_set/DELETE' A) s x) t)))).
tt('thm/pred_set/DIFF_INSERT_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/DIFF' A) s (('const/pred_set/INSERT' A) x t)) = (('const/pred_set/DIFF' A) (('const/pred_set/DELETE' A) s x) t)))).
tt('thm/pred_set/PSUBSET_INSERT_SUBSET_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/PSUBSET' A) s t) = (?[x : A]: ((~ (('const/bool/IN' A) x s)) & (('const/pred_set/SUBSET' A) (('const/pred_set/INSERT' A) x s) t)))))).
tt('thm/pred_set/PSUBSET_MEMBER_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/PSUBSET' A) s t) = ((('const/pred_set/SUBSET' A) s t) & (?[y : A]: ((('const/bool/IN' A) y t) & (~ (('const/bool/IN' A) y s)))))))).
tt('thm/pred_set/DELETE_INSERT_', ax, ![A : $t]: (![x : A, y : A, s : (A > $o)]: ((('const/pred_set/DELETE' A) (('const/pred_set/INSERT' A) x s) y) = (('const/bool/COND' (A > $o)) (x = y) (('const/pred_set/DELETE' A) s y) (('const/pred_set/INSERT' A) x (('const/pred_set/DELETE' A) s y)))))).
tt('thm/pred_set/INSERT_DELETE_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/bool/IN' A) x s) => ((('const/pred_set/INSERT' A) x (('const/pred_set/DELETE' A) s x)) = s)))).
tt('thm/pred_set/DELETE_INTER_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/INTER' A) (('const/pred_set/DELETE' A) s x) t) = (('const/pred_set/DELETE' A) (('const/pred_set/INTER' A) s t) x)))).
tt('thm/pred_set/DISJOINT_DELETE_SYM_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), x : A]: ((('const/pred_set/DISJOINT' A) (('const/pred_set/DELETE' A) s x) t) = (('const/pred_set/DISJOINT' A) (('const/pred_set/DELETE' A) t x) s)))).
tt('thm/pred_set/CHOICE_DEF_', def, ![A : $t]: (![s : (A > $o)]: ((~ (s = ('const/pred_set/EMPTY' A))) => (('const/bool/IN' A) (('const/pred_set/CHOICE' A) s) s)))).
tt('thm/pred_set/REST_DEF_', def, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/REST' A) s) = (('const/pred_set/DELETE' A) s (('const/pred_set/CHOICE' A) s))))).
tt('thm/pred_set/CHOICE_NOT_IN_REST_', ax, ![A : $t]: (![s : (A > $o)]: (~ (('const/bool/IN' A) (('const/pred_set/CHOICE' A) s) (('const/pred_set/REST' A) s))))).
tt('thm/pred_set/CHOICE_INSERT_REST_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (s = ('const/pred_set/EMPTY' A))) => ((('const/pred_set/INSERT' A) (('const/pred_set/CHOICE' A) s) (('const/pred_set/REST' A) s)) = s)))).
tt('thm/pred_set/REST_SUBSET_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/SUBSET' A) (('const/pred_set/REST' A) s) s))).
tt('thm/pred_set/REST_PSUBSET_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (s = ('const/pred_set/EMPTY' A))) => (('const/pred_set/PSUBSET' A) (('const/pred_set/REST' A) s) s)))).
tt('thm/pred_set/SING_DEF_', def, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/SING' A) s) = (?[x : A]: (s = (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))))).
tt('thm/pred_set/SING_', ax, ![A : $t]: (![x : A]: (('const/pred_set/SING' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/SING_EMPTY_', ax, ![A : $t]: ((('const/pred_set/SING' A) ('const/pred_set/EMPTY' A)) = $false)).
tt('thm/pred_set/SING_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/SING' A) (('const/pred_set/INSERT' A) x s)) = ((s = ('const/pred_set/EMPTY' A)) | (s = (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))))).
tt('thm/pred_set/SING_UNION_', ax, ![A : $t]: (![t : (A > $o), s : (A > $o)]: ((('const/pred_set/SING' A) (('const/pred_set/UNION' A) s t)) = (((('const/pred_set/SING' A) s) & (t = ('const/pred_set/EMPTY' A))) | (((('const/pred_set/SING' A) t) & (s = ('const/pred_set/EMPTY' A))) | ((('const/pred_set/SING' A) s) & ((('const/pred_set/SING' A) t) & (s = t)))))))).
tt('thm/pred_set/IN_SING_', ax, ![A : $t]: (![x : A, y : A]: ((('const/bool/IN' A) x (('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A))) = (x = y)))).
tt('thm/pred_set/SING_applied_', ax, ![A : $t]: (![x : A, y : A]: ((('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A) x) = (x = y)))).
tt('thm/pred_set/NOT_SING_EMPTY_', ax, ![A : $t]: (![x : A]: (~ ((('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/NOT_EMPTY_SING_', ax, ![A : $t]: (![x : A]: (~ (('const/pred_set/EMPTY' A) = (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/EQUAL_SING_', ax, ![A : $t]: (![x : A, y : A]: (((('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) = (('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A))) = (x = y)))).
tt('thm/pred_set/DISJOINT_SING_EMPTY_', ax, ![A : $t]: (![x : A]: (('const/pred_set/DISJOINT' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/INSERT_SING_UNION_', ax, ![A : $t]: (![s : (A > $o), x : A]: ((('const/pred_set/INSERT' A) x s) = (('const/pred_set/UNION' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) s)))).
tt('thm/pred_set/SING_DELETE_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/DELETE' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) x) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/DELETE_EQ_SING_', ax, ![A : $t]: (![s : (A > $o), x : A]: ((('const/bool/IN' A) x s) => (((('const/pred_set/DELETE' A) s x) = ('const/pred_set/EMPTY' A)) = (s = (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))))).
tt('thm/pred_set/CHOICE_SING_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/CHOICE' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) = x))).
tt('thm/pred_set/REST_SING_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/REST' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/SING_IFF_EMPTY_REST_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/SING' A) s) = ((~ (s = ('const/pred_set/EMPTY' A))) & ((('const/pred_set/REST' A) s) = ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/IMAGE_DEF_', def, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: ((('const/pred_set/IMAGE' A B) f s) = (('const/pred_set/GSPEC' B A) (^[x : A]: (('const/pair/,' B $o) (f x) (('const/bool/IN' A) x s))))))).
tt('thm/pred_set/IN_IMAGE_', ax, ![A : $t, B : $t]: (![y : B, s : (A > $o), f : (A > B)]: ((('const/bool/IN' B) y (('const/pred_set/IMAGE' A B) f s)) = (?[x : A]: ((y = (f x)) & (('const/bool/IN' A) x s)))))).
tt('thm/pred_set/IMAGE_applied_', ax, ![A : $t, B : $t]: (![y : B, s : (A > $o), f : (A > B)]: ((('const/pred_set/IMAGE' A B) f s y) = (?[x : A]: ((y = (f x)) & (('const/bool/IN' A) x s)))))).
tt('thm/pred_set/IMAGE_IN_', ax, ![A : $t, B : $t]: (![x : A, s : (A > $o)]: ((('const/bool/IN' A) x s) => (![f : (A > B)]: (('const/bool/IN' B) (f x) (('const/pred_set/IMAGE' A B) f s)))))).
tt('thm/pred_set/IMAGE_EMPTY_', ax, ![B : $t, A : $t]: (![f : (A > B)]: ((('const/pred_set/IMAGE' A B) f ('const/pred_set/EMPTY' A)) = ('const/pred_set/EMPTY' B)))).
tt('thm/pred_set/IMAGE_ID_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/IMAGE' A A) (^[x : A]: x) s) = s))).
tt('thm/pred_set/IMAGE_COMPOSE_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), g : (A > B), s : (A > $o)]: ((('const/pred_set/IMAGE' A C) (('const/combin/o' A C B) f g) s) = (('const/pred_set/IMAGE' B C) f (('const/pred_set/IMAGE' A B) g s))))).
tt('thm/pred_set/IMAGE_INSERT_', ax, ![A : $t, B : $t]: (![f : (A > B), x : A, s : (A > $o)]: ((('const/pred_set/IMAGE' A B) f (('const/pred_set/INSERT' A) x s)) = (('const/pred_set/INSERT' B) (f x) (('const/pred_set/IMAGE' A B) f s))))).
tt('thm/pred_set/IMAGE_EQ_EMPTY_', ax, ![A : $t, B : $t]: (![s : (A > $o), f : (A > B)]: (((('const/pred_set/IMAGE' A B) f s) = ('const/pred_set/EMPTY' B)) = (s = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/IMAGE_DELETE_', ax, ![A : $t, B : $t]: (![f : (A > B), x : A, s : (A > $o)]: ((~ (('const/bool/IN' A) x s)) => ((('const/pred_set/IMAGE' A B) f (('const/pred_set/DELETE' A) s x)) = (('const/pred_set/IMAGE' A B) f s))))).
tt('thm/pred_set/IMAGE_UNION_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (A > $o)]: ((('const/pred_set/IMAGE' A B) f (('const/pred_set/UNION' A) s t)) = (('const/pred_set/UNION' B) (('const/pred_set/IMAGE' A B) f s) (('const/pred_set/IMAGE' A B) f t))))).
tt('thm/pred_set/IMAGE_SUBSET_', ax, ![A : $t, B : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) s t) => (![f : (A > B)]: (('const/pred_set/SUBSET' B) (('const/pred_set/IMAGE' A B) f s) (('const/pred_set/IMAGE' A B) f t)))))).
tt('thm/pred_set/IMAGE_INTER_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (A > $o)]: (('const/pred_set/SUBSET' B) (('const/pred_set/IMAGE' A B) f (('const/pred_set/INTER' A) s t)) (('const/pred_set/INTER' B) (('const/pred_set/IMAGE' A B) f s) (('const/pred_set/IMAGE' A B) f t))))).
tt('thm/pred_set/IMAGE_11_', ax, ![A : $t, B : $t]: (![s2 : (A > $o), s1 : (A > $o), f : (A > B)]: ((![x : A, y : A]: (((f x) = (f y)) = (x = y))) => (((('const/pred_set/IMAGE' A B) f s1) = (('const/pred_set/IMAGE' A B) f s2)) = (s1 = s2))))).
tt('thm/pred_set/IMAGE_CONG_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), 'f\'' : (A > B), 's\'' : (A > $o)]: (((s = 's\'') & (![x : A]: ((('const/bool/IN' A) x 's\'') => ((f x) = ('f\'' x))))) => ((('const/pred_set/IMAGE' A B) f s) = (('const/pred_set/IMAGE' A B) 'f\'' 's\''))))).
tt('thm/pred_set/INJ_DEF_', def, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/INJ' A B) f s t) = ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' B) (f x) t))) & (![x : A, y : A]: (((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)) => (((f x) = (f y)) => (x = y)))))))).
tt('thm/pred_set/INJ_IFF_', ax, ![A : $t, B : $t]: (![t : (B > $o), s : (A > $o), f : (A > B)]: ((('const/pred_set/INJ' A B) f s t) = ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' B) (f x) t))) & (![x : A, y : A]: (((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)) => (((f x) = (f y)) = (x = y)))))))).
tt('thm/pred_set/INJ_ID_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/INJ' A A) (^[x : A]: x) s s))).
tt('thm/pred_set/INJ_COMPOSE_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (B > C), s : (A > $o), t : (B > $o), u : (C > $o)]: (((('const/pred_set/INJ' A B) f s t) & (('const/pred_set/INJ' B C) g t u)) => (('const/pred_set/INJ' A C) (('const/combin/o' A C B) g f) s u)))).
tt('thm/pred_set/INJ_EMPTY_0', ax, ![B : $t, A : $t]: (![f : (A > B), s : (B > $o)]: (('const/pred_set/INJ' A B) f ('const/pred_set/EMPTY' A) s))).
tt('thm/pred_set/INJ_EMPTY_e1', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: ((('const/pred_set/INJ' A B) f s ('const/pred_set/EMPTY' B)) = (s = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/INJ_DELETE_', ax, ![A : $t, B : $t]: (![s : (A > $o), t : (B > $o), f : (A > B)]: ((('const/pred_set/INJ' A B) f s t) => (![e : A]: ((('const/bool/IN' A) e s) => (('const/pred_set/INJ' A B) f (('const/pred_set/DELETE' A) s e) (('const/pred_set/DELETE' B) t (f e)))))))).
tt('thm/pred_set/INJ_INSERT_', ax, ![A : $t, B : $t]: (![f : (A > B), x : A, s : (A > $o), t : (B > $o)]: ((('const/pred_set/INJ' A B) f (('const/pred_set/INSERT' A) x s) t) = ((('const/pred_set/INJ' A B) f s t) & ((('const/bool/IN' B) (f x) t) & (![y : A]: (((('const/bool/IN' A) y s) & ((f x) = (f y))) => (x = y)))))))).
tt('thm/pred_set/INJ_SUBSET_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o), s0 : (A > $o), t0 : (B > $o)]: (((('const/pred_set/INJ' A B) f s t) & ((('const/pred_set/SUBSET' A) s0 s) & (('const/pred_set/SUBSET' B) t t0))) => (('const/pred_set/INJ' A B) f s0 t0)))).
tt('thm/pred_set/SURJ_DEF_', def, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/SURJ' A B) f s t) = ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' B) (f x) t))) & (![x : B]: ((('const/bool/IN' B) x t) => (?[y : A]: ((('const/bool/IN' A) y s) & ((f y) = x))))))))).
tt('thm/pred_set/SURJ_ID_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/SURJ' A A) (^[x : A]: x) s s))).
tt('thm/pred_set/SURJ_COMPOSE_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (B > C), s : (A > $o), t : (B > $o), u : (C > $o)]: (((('const/pred_set/SURJ' A B) f s t) & (('const/pred_set/SURJ' B C) g t u)) => (('const/pred_set/SURJ' A C) (('const/combin/o' A C B) g f) s u)))).
tt('thm/pred_set/SURJ_EMPTY_0', ax, ![B : $t, A : $t]: (![f : (A > B), s : (B > $o)]: ((('const/pred_set/SURJ' A B) f ('const/pred_set/EMPTY' A) s) = (s = ('const/pred_set/EMPTY' B))))).
tt('thm/pred_set/SURJ_EMPTY_e1', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: ((('const/pred_set/SURJ' A B) f s ('const/pred_set/EMPTY' B)) = (s = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/IMAGE_SURJ_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/SURJ' A B) f s t) = ((('const/pred_set/IMAGE' A B) f s) = t)))).
tt('thm/pred_set/SURJ_IMAGE_', ax, ![A : $t, B : $t]: (![s : (A > $o), f : (A > B)]: (('const/pred_set/SURJ' A B) f s (('const/pred_set/IMAGE' A B) f s)))).
tt('thm/pred_set/SURJ_INJ_INV_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o), f : (A > B)]: ((('const/pred_set/SURJ' A B) f s t) => (?[g : (B > A)]: ((('const/pred_set/INJ' B A) g t s) & (![y : B]: ((('const/bool/IN' B) y t) => ((f (g y)) = y)))))))).
tt('thm/pred_set/BIJ_DEF_', def, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/BIJ' A B) f s t) = ((('const/pred_set/INJ' A B) f s t) & (('const/pred_set/SURJ' A B) f s t))))).
tt('thm/pred_set/BIJ_ID_', ax, ![A : $t]: (![s : (A > $o)]: (('const/pred_set/BIJ' A A) (^[x : A]: x) s s))).
tt('thm/pred_set/BIJ_EMPTY_0', ax, ![B : $t, A : $t]: (![f : (A > B), s : (B > $o)]: ((('const/pred_set/BIJ' A B) f ('const/pred_set/EMPTY' A) s) = (s = ('const/pred_set/EMPTY' B))))).
tt('thm/pred_set/BIJ_EMPTY_e1', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: ((('const/pred_set/BIJ' A B) f s ('const/pred_set/EMPTY' B)) = (s = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/BIJ_COMPOSE_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (B > C), s : (A > $o), t : (B > $o), u : (C > $o)]: (((('const/pred_set/BIJ' A B) f s t) & (('const/pred_set/BIJ' B C) g t u)) => (('const/pred_set/BIJ' A C) (('const/combin/o' A C B) g f) s u)))).
tt('thm/pred_set/BIJ_DELETE_', ax, ![A : $t, B : $t]: (![s : (A > $o), t : (B > $o), f : (A > B)]: ((('const/pred_set/BIJ' A B) f s t) => (![e : A]: ((('const/bool/IN' A) e s) => (('const/pred_set/BIJ' A B) f (('const/pred_set/DELETE' A) s e) (('const/pred_set/DELETE' B) t (f e)))))))).
tt('thm/pred_set/LINV_DEF_', def, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/INJ' A B) f s t) => (![x : A]: ((('const/bool/IN' A) x s) => ((('const/pred_set/LINV' A B) f s (f x)) = x)))))).
tt('thm/pred_set/BIJ_LINV_INV_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/BIJ' A B) f s t) => (![x : B]: ((('const/bool/IN' B) x t) => ((f (('const/pred_set/LINV' A B) f s x)) = x)))))).
tt('thm/pred_set/BIJ_LINV_BIJ_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/BIJ' A B) f s t) => (('const/pred_set/BIJ' B A) (('const/pred_set/LINV' A B) f s) t s)))).
tt('thm/pred_set/BIJ_IFF_INV_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/BIJ' A B) f s t) = ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' B) (f x) t))) & (?[g : (B > A)]: ((![x : B]: ((('const/bool/IN' B) x t) => (('const/bool/IN' A) (g x) s))) & ((![x : A]: ((('const/bool/IN' A) x s) => ((g (f x)) = x))) & (![x : B]: ((('const/bool/IN' B) x t) => ((f (g x)) = x)))))))))).
tt('thm/pred_set/BIJ_INSERT_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o), f : (A > B), e : A]: ((('const/pred_set/BIJ' A B) f (('const/pred_set/INSERT' A) e s) t) = (((~ (('const/bool/IN' A) e s)) & ((('const/bool/IN' B) (f e) t) & (('const/pred_set/BIJ' A B) f s (('const/pred_set/DELETE' B) t (f e))))) | ((('const/bool/IN' A) e s) & (('const/pred_set/BIJ' A B) f s t)))))).
tt('thm/pred_set/RINV_DEF_', def, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/SURJ' A B) f s t) => (![x : B]: ((('const/bool/IN' B) x t) => ((f (('const/pred_set/RINV' A B) f s x)) = x)))))).
tt('thm/pred_set/FINITE_DEF_', def, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) = (![P : ((A > $o) > $o)]: (((P ('const/pred_set/EMPTY' A)) & (![s0 : (A > $o)]: ((P s0) => (![e : A]: (P (('const/pred_set/INSERT' A) e s0)))))) => (P s)))))).
tt('thm/pred_set/FINITE_EMPTY_', ax, ![A : $t]: (('const/pred_set/FINITE' A) ('const/pred_set/EMPTY' A))).
tt('thm/pred_set/FINITE_INDUCT_', ax, ![A : $t]: (![P : ((A > $o) > $o)]: (((P ('const/pred_set/EMPTY' A)) & (![s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (P s)) => (![e : A]: ((~ (('const/bool/IN' A) e s)) => (P (('const/pred_set/INSERT' A) e s))))))) => (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (P s)))))).
tt('thm/pred_set/FINITE_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/FINITE' A) (('const/pred_set/INSERT' A) x s)) = (('const/pred_set/FINITE' A) s)))).
tt('thm/pred_set/FINITE_DELETE_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/FINITE' A) (('const/pred_set/DELETE' A) s x)) = (('const/pred_set/FINITE' A) s)))).
tt('thm/pred_set/FINITE_REST_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (('const/pred_set/FINITE' A) (('const/pred_set/REST' A) s))))).
tt('thm/pred_set/FINITE_UNION_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/FINITE' A) (('const/pred_set/UNION' A) s t)) = ((('const/pred_set/FINITE' A) s) & (('const/pred_set/FINITE' A) t))))).
tt('thm/pred_set/INTER_FINITE_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: (('const/pred_set/FINITE' A) (('const/pred_set/INTER' A) s t)))))).
tt('thm/pred_set/SUBSET_FINITE_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: ((('const/pred_set/SUBSET' A) t s) => (('const/pred_set/FINITE' A) t)))))).
tt('thm/pred_set/SUBSET_FINITE_I_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (('const/pred_set/SUBSET' A) t s)) => (('const/pred_set/FINITE' A) t)))).
tt('thm/pred_set/PSUBSET_FINITE_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: ((('const/pred_set/PSUBSET' A) t s) => (('const/pred_set/FINITE' A) t)))))).
tt('thm/pred_set/FINITE_DIFF_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: (('const/pred_set/FINITE' A) (('const/pred_set/DIFF' A) s t)))))).
tt('thm/pred_set/FINITE_DIFF_down_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o)]: (((('const/pred_set/FINITE' A) (('const/pred_set/DIFF' A) P Q)) & (('const/pred_set/FINITE' A) Q)) => (('const/pred_set/FINITE' A) P)))).
tt('thm/pred_set/FINITE_SING_', ax, ![A : $t]: (![x : A]: (('const/pred_set/FINITE' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/SING_FINITE_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/SING' A) s) => (('const/pred_set/FINITE' A) s)))).
tt('thm/pred_set/IMAGE_FINITE_', ax, ![A : $t, B : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > B)]: (('const/pred_set/FINITE' B) (('const/pred_set/IMAGE' A B) f s)))))).
tt('thm/pred_set/FINITELY_INJECTIVE_IMAGE_FINITE_', ax, ![A : $t, B : $t]: (![f : (A > B)]: ((![x : B]: (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (x = (f y))))))) => (![s : (A > $o)]: ((('const/pred_set/FINITE' B) (('const/pred_set/IMAGE' A B) f s)) = (('const/pred_set/FINITE' A) s)))))).
tt('thm/pred_set/INJECTIVE_IMAGE_FINITE_', ax, ![A : $t, B : $t]: (![f : (A > B)]: ((![x : A, y : A]: (((f x) = (f y)) = (x = y))) => (![s : (A > $o)]: ((('const/pred_set/FINITE' B) (('const/pred_set/IMAGE' A B) f s)) = (('const/pred_set/FINITE' A) s)))))).
tt('thm/pred_set/FINITE_INJ_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: (((('const/pred_set/INJ' A B) f s t) & (('const/pred_set/FINITE' B) t)) => (('const/pred_set/FINITE' A) s)))).
tt('thm/pred_set/REL_RESTRICT_DEF_', def, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o), x : A, y : A]: ((('const/pred_set/REL_RESTRICT' A) R s x y) = ((('const/bool/IN' A) x s) & ((('const/bool/IN' A) y s) & (R x y)))))).
tt('thm/pred_set/REL_RESTRICT_EMPTY_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/pred_set/REL_RESTRICT' A) R ('const/pred_set/EMPTY' A)) = ('const/relation/EMPTY_REL' A)))).
tt('thm/pred_set/REL_RESTRICT_SUBSET_', ax, ![A : $t]: (![s2 : (A > $o), s1 : (A > $o), R : (A > (A > $o))]: ((('const/pred_set/SUBSET' A) s1 s2) => (('const/relation/RSUBSET' A A) (('const/pred_set/REL_RESTRICT' A) R s1) (('const/pred_set/REL_RESTRICT' A) R s2))))).
tt('thm/pred_set/CARD_DEF_0', def, ![A : $t]: ((('const/pred_set/CARD' A) ('const/pred_set/EMPTY' A)) = 'const/num/0')).
tt('thm/pred_set/CARD_DEF_e1', def, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![x : A]: ((('const/pred_set/CARD' A) (('const/pred_set/INSERT' A) x s)) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' A) x s) (('const/pred_set/CARD' A) s) ('const/num/SUC' (('const/pred_set/CARD' A) s)))))))).
tt('thm/pred_set/CARD_EMPTY_', ax, ![A : $t]: ((('const/pred_set/CARD' A) ('const/pred_set/EMPTY' A)) = 'const/num/0')).
tt('thm/pred_set/CARD_INSERT_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![x : A]: ((('const/pred_set/CARD' A) (('const/pred_set/INSERT' A) x s)) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' A) x s) (('const/pred_set/CARD' A) s) ('const/num/SUC' (('const/pred_set/CARD' A) s)))))))).
tt('thm/pred_set/CARD_EQ_0_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (((('const/pred_set/CARD' A) s) = 'const/num/0') = (s = ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/CARD_DELETE_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![x : A]: ((('const/pred_set/CARD' A) (('const/pred_set/DELETE' A) s x)) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' A) x s) ('const/arithmetic/-' (('const/pred_set/CARD' A) s) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/pred_set/CARD' A) s))))))).
tt('thm/pred_set/CARD_INTER_LESS_EQ_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: ('const/arithmetic/<=' (('const/pred_set/CARD' A) (('const/pred_set/INTER' A) s t)) (('const/pred_set/CARD' A) s)))))).
tt('thm/pred_set/CARD_UNION_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: ((('const/pred_set/FINITE' A) t) => (('const/arithmetic/+' (('const/pred_set/CARD' A) (('const/pred_set/UNION' A) s t)) (('const/pred_set/CARD' A) (('const/pred_set/INTER' A) s t))) = ('const/arithmetic/+' (('const/pred_set/CARD' A) s) (('const/pred_set/CARD' A) t)))))))).
tt('thm/pred_set/CARD_UNION_EQN_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (('const/pred_set/FINITE' A) t)) => ((('const/pred_set/CARD' A) (('const/pred_set/UNION' A) s t)) = ('const/arithmetic/-' ('const/arithmetic/+' (('const/pred_set/CARD' A) s) (('const/pred_set/CARD' A) t)) (('const/pred_set/CARD' A) (('const/pred_set/INTER' A) s t))))))).
tt('thm/pred_set/CARD_SUBSET_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: ((('const/pred_set/SUBSET' A) t s) => ('const/arithmetic/<=' (('const/pred_set/CARD' A) t) (('const/pred_set/CARD' A) s))))))).
tt('thm/pred_set/CARD_PSUBSET_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: ((('const/pred_set/PSUBSET' A) t s) => ('const/prim_rec/<' (('const/pred_set/CARD' A) t) (('const/pred_set/CARD' A) s))))))).
tt('thm/pred_set/SUBSET_EQ_CARD_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![t : (A > $o)]: (((('const/pred_set/FINITE' A) t) & (((('const/pred_set/CARD' A) s) = (('const/pred_set/CARD' A) t)) & (('const/pred_set/SUBSET' A) s t))) => (s = t)))))).
tt('thm/pred_set/CARD_SING_', ax, ![A : $t]: (![x : A]: ((('const/pred_set/CARD' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/pred_set/SING_IFF_CARD1_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/SING' A) s) = (((('const/pred_set/CARD' A) s) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (('const/pred_set/FINITE' A) s))))).
tt('thm/pred_set/CARD_DIFF_', ax, ![A : $t]: (![t : (A > $o)]: ((('const/pred_set/FINITE' A) t) => (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/CARD' A) (('const/pred_set/DIFF' A) s t)) = ('const/arithmetic/-' (('const/pred_set/CARD' A) s) (('const/pred_set/CARD' A) (('const/pred_set/INTER' A) s t))))))))).
tt('thm/pred_set/CARD_DIFF_EQN_', ax, ![A : $t]: (![t : (A > $o), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/CARD' A) (('const/pred_set/DIFF' A) s t)) = ('const/arithmetic/-' (('const/pred_set/CARD' A) s) (('const/pred_set/CARD' A) (('const/pred_set/INTER' A) s t))))))).
tt('thm/pred_set/LESS_CARD_DIFF_', ax, ![A : $t]: (![t : (A > $o)]: ((('const/pred_set/FINITE' A) t) => (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (('const/prim_rec/<' (('const/pred_set/CARD' A) t) (('const/pred_set/CARD' A) s)) => ('const/prim_rec/<' 'const/num/0' (('const/pred_set/CARD' A) (('const/pred_set/DIFF' A) s t))))))))).
tt('thm/pred_set/BIJ_FINITE_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: (((('const/pred_set/BIJ' A B) f s t) & (('const/pred_set/FINITE' A) s)) => (('const/pred_set/FINITE' B) t)))).
tt('thm/pred_set/FINITE_BIJ_CARD_EQ_', ax, ![B : $t, A : $t]: (![S : (A > $o)]: ((('const/pred_set/FINITE' A) S) => (![t : (B > $o), f : (A > B)]: (((('const/pred_set/BIJ' A B) f S t) & (('const/pred_set/FINITE' B) t)) => ((('const/pred_set/CARD' A) S) = (('const/pred_set/CARD' B) t))))))).
tt('thm/pred_set/CARD_INJ_IMAGE_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: (((![x : A, y : A]: (((f x) = (f y)) = (x = y))) & (('const/pred_set/FINITE' A) s)) => ((('const/pred_set/CARD' B) (('const/pred_set/IMAGE' A B) f s)) = (('const/pred_set/CARD' A) s))))).
tt('thm/pred_set/FINITE_COMPLETE_INDUCTION_', ax, ![A : $t]: (![P : ((A > $o) > $o)]: ((![x : (A > $o)]: ((![y : (A > $o)]: ((('const/pred_set/PSUBSET' A) y x) => (P y))) => ((('const/pred_set/FINITE' A) x) => (P x)))) => (![x : (A > $o)]: ((('const/pred_set/FINITE' A) x) => (P x)))))).
tt('thm/pred_set/INJ_CARD_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: (((('const/pred_set/INJ' A B) f s t) & (('const/pred_set/FINITE' B) t)) => ('const/arithmetic/<=' (('const/pred_set/CARD' A) s) (('const/pred_set/CARD' B) t))))).
tt('thm/pred_set/PHP_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: (((('const/pred_set/FINITE' B) t) & ('const/prim_rec/<' (('const/pred_set/CARD' B) t) (('const/pred_set/CARD' A) s))) => (~ (('const/pred_set/INJ' A B) f s t))))).
tt('thm/pred_set/INFINITE_DEF_', ax, $true).
tt('thm/pred_set/NOT_IN_FINITE_', ax, ![A : $t]: ((~ (('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A))) = (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (?[x : A]: (~ (('const/bool/IN' A) x s))))))).
tt('thm/pred_set/INFINITE_INHAB_', ax, ![A : $t]: (![P : (A > $o)]: ((~ (('const/pred_set/FINITE' A) P)) => (?[x : A]: (('const/bool/IN' A) x P))))).
tt('thm/pred_set/IMAGE_11_INFINITE_', ax, ![A : $t, B : $t]: (![f : (A > B)]: ((![x : A, y : A]: (((f x) = (f y)) => (x = y))) => (![s : (A > $o)]: ((~ (('const/pred_set/FINITE' A) s)) => (~ (('const/pred_set/FINITE' B) (('const/pred_set/IMAGE' A B) f s)))))))).
tt('thm/pred_set/INFINITE_SUBSET_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (('const/pred_set/FINITE' A) s)) => (![t : (A > $o)]: ((('const/pred_set/SUBSET' A) s t) => (~ (('const/pred_set/FINITE' A) t))))))).
tt('thm/pred_set/IN_INFINITE_NOT_FINITE_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((~ (('const/pred_set/FINITE' A) s)) & (('const/pred_set/FINITE' A) t)) => (?[x : A]: ((('const/bool/IN' A) x s) & (~ (('const/bool/IN' A) x t))))))).
tt('thm/pred_set/INFINITE_UNIV_', ax, ![A : $t]: ((~ (('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A))) = (?[f : (A > A)]: ((![x : A, y : A]: (((f x) = (f y)) => (x = y))) & (?[y : A]: (![x : A]: (~ ((f x) = y)))))))).
tt('thm/pred_set/INFINITE_NUM_UNIV_', ax, (~ (('const/pred_set/FINITE' 'type/num/num') ('const/pred_set/UNIV' 'type/num/num')))).
tt('thm/pred_set/FINITE_PSUBSET_INFINITE_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (('const/pred_set/FINITE' A) s)) = (![t : (A > $o)]: ((('const/pred_set/FINITE' A) t) => ((('const/pred_set/SUBSET' A) t s) => (('const/pred_set/PSUBSET' A) t s))))))).
tt('thm/pred_set/FINITE_PSUBSET_UNIV_', ax, ![A : $t]: ((~ (('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A))) = (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (('const/pred_set/PSUBSET' A) s ('const/pred_set/UNIV' A)))))).
tt('thm/pred_set/INFINITE_DIFF_FINITE_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((~ (('const/pred_set/FINITE' A) s)) & (('const/pred_set/FINITE' A) t)) => (~ ((('const/pred_set/DIFF' A) s t) = ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/FINITE_ISO_NUM_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (?[f : ('type/num/num' > A)]: ((![n : 'type/num/num', m : 'type/num/num']: ((('const/prim_rec/<' n (('const/pred_set/CARD' A) s)) & ('const/prim_rec/<' m (('const/pred_set/CARD' A) s))) => (((f n) = (f m)) => (n = m)))) & (s = (('const/pred_set/GSPEC' A 'type/num/num') (^[n : 'type/num/num']: (('const/pair/,' A $o) (f n) ('const/prim_rec/<' n (('const/pred_set/CARD' A) s))))))))))).
tt('thm/pred_set/FINITE_WEAK_ENUMERATE_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) = (?[f : ('type/num/num' > A), b : 'type/num/num']: (![e : A]: ((('const/bool/IN' A) e s) = (?[n : 'type/num/num']: (('const/prim_rec/<' n b) & (e = (f n)))))))))).
tt('thm/pred_set/FINITE_WF_noloops_', ax, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/relation/WF' A) (('const/pred_set/REL_RESTRICT' A) R s)) = (('const/relation/irreflexive' A) (('const/relation/TC' A) (('const/pred_set/REL_RESTRICT' A) R s))))))).
tt('thm/pred_set/FINITE_StrongOrder_WF_', ax, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (('const/relation/StrongOrder' A) (('const/pred_set/REL_RESTRICT' A) R s))) => (('const/relation/WF' A) (('const/pred_set/REL_RESTRICT' A) R s))))).
tt('thm/pred_set/BIGUNION_', def, ![A : $t]: (![P : ((A > $o) > $o)]: ((('const/pred_set/BIGUNION' A) P) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (?[s : (A > $o)]: ((('const/bool/IN' (A > $o)) s P) & (('const/bool/IN' A) x s))))))))).
tt('thm/pred_set/IN_BIGUNION_', ax, ![A : $t]: (![x : A, sos : ((A > $o) > $o)]: ((('const/bool/IN' A) x (('const/pred_set/BIGUNION' A) sos)) = (?[s : (A > $o)]: ((('const/bool/IN' A) x s) & (('const/bool/IN' (A > $o)) s sos)))))).
tt('thm/pred_set/BIGUNION_applied_', ax, ![A : $t]: (![x : A, sos : ((A > $o) > $o)]: ((('const/pred_set/BIGUNION' A) sos x) = (?[s : (A > $o)]: ((('const/bool/IN' A) x s) & (('const/bool/IN' (A > $o)) s sos)))))).
tt('thm/pred_set/BIGUNION_EMPTY_', ax, ![A : $t]: ((('const/pred_set/BIGUNION' A) ('const/pred_set/EMPTY' (A > $o))) = ('const/pred_set/EMPTY' A))).
tt('thm/pred_set/BIGUNION_EQ_EMPTY_0', ax, ![A : $t]: (![P : ((A > $o) > $o)]: (((('const/pred_set/BIGUNION' A) P) = ('const/pred_set/EMPTY' A)) = ((P = ('const/pred_set/EMPTY' (A > $o))) | (P = (('const/pred_set/INSERT' (A > $o)) ('const/pred_set/EMPTY' A) ('const/pred_set/EMPTY' (A > $o)))))))).
tt('thm/pred_set/BIGUNION_EQ_EMPTY_e1', ax, ![A : $t]: (![P : ((A > $o) > $o)]: ((('const/pred_set/EMPTY' A) = (('const/pred_set/BIGUNION' A) P)) = ((P = ('const/pred_set/EMPTY' (A > $o))) | (P = (('const/pred_set/INSERT' (A > $o)) ('const/pred_set/EMPTY' A) ('const/pred_set/EMPTY' (A > $o)))))))).
tt('thm/pred_set/BIGUNION_SING_', ax, ![A : $t]: (![x : (A > $o)]: ((('const/pred_set/BIGUNION' A) (('const/pred_set/INSERT' (A > $o)) x ('const/pred_set/EMPTY' (A > $o)))) = x))).
tt('thm/pred_set/BIGUNION_UNION_', ax, ![A : $t]: (![s1 : ((A > $o) > $o), s2 : ((A > $o) > $o)]: ((('const/pred_set/BIGUNION' A) (('const/pred_set/UNION' (A > $o)) s1 s2)) = (('const/pred_set/UNION' A) (('const/pred_set/BIGUNION' A) s1) (('const/pred_set/BIGUNION' A) s2))))).
tt('thm/pred_set/DISJOINT_BIGUNION_0', ax, ![A : $t]: (![s : ((A > $o) > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) (('const/pred_set/BIGUNION' A) s) t) = (!['s\'' : (A > $o)]: ((('const/bool/IN' (A > $o)) 's\'' s) => (('const/pred_set/DISJOINT' A) 's\'' t)))))).
tt('thm/pred_set/DISJOINT_BIGUNION_e1', ax, ![A : $t]: (![s : ((A > $o) > $o), t : (A > $o)]: ((('const/pred_set/DISJOINT' A) t (('const/pred_set/BIGUNION' A) s)) = (!['s\'' : (A > $o)]: ((('const/bool/IN' (A > $o)) 's\'' s) => (('const/pred_set/DISJOINT' A) t 's\'')))))).
tt('thm/pred_set/BIGUNION_INSERT_', ax, ![A : $t]: (![s : (A > $o), P : ((A > $o) > $o)]: ((('const/pred_set/BIGUNION' A) (('const/pred_set/INSERT' (A > $o)) s P)) = (('const/pred_set/UNION' A) s (('const/pred_set/BIGUNION' A) P))))).
tt('thm/pred_set/BIGUNION_SUBSET_', ax, ![A : $t]: (![X : (A > $o), P : ((A > $o) > $o)]: ((('const/pred_set/SUBSET' A) (('const/pred_set/BIGUNION' A) P) X) = (![Y : (A > $o)]: ((('const/bool/IN' (A > $o)) Y P) => (('const/pred_set/SUBSET' A) Y X)))))).
tt('thm/pred_set/FINITE_BIGUNION_', ax, ![A : $t]: (![P : ((A > $o) > $o)]: (((('const/pred_set/FINITE' (A > $o)) P) & (![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s P) => (('const/pred_set/FINITE' A) s)))) => (('const/pred_set/FINITE' A) (('const/pred_set/BIGUNION' A) P))))).
tt('thm/pred_set/FINITE_BIGUNION_EQ_', ax, ![A : $t]: (![P : ((A > $o) > $o)]: ((('const/pred_set/FINITE' A) (('const/pred_set/BIGUNION' A) P)) = ((('const/pred_set/FINITE' (A > $o)) P) & (![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s P) => (('const/pred_set/FINITE' A) s))))))).
tt('thm/pred_set/SUBSET_BIGUNION_I_', ax, ![A : $t]: (![x : (A > $o), P : ((A > $o) > $o)]: ((('const/bool/IN' (A > $o)) x P) => (('const/pred_set/SUBSET' A) x (('const/pred_set/BIGUNION' A) P))))).
tt('thm/pred_set/CARD_BIGUNION_SAME_SIZED_SETS_', ax, ![A : $t]: (![n : 'type/num/num', s : ((A > $o) > $o)]: (((('const/pred_set/FINITE' (A > $o)) s) & ((![e : (A > $o)]: ((('const/bool/IN' (A > $o)) e s) => ((('const/pred_set/FINITE' A) e) & ((('const/pred_set/CARD' A) e) = n)))) & (![e1 : (A > $o), e2 : (A > $o)]: (((('const/bool/IN' (A > $o)) e1 s) & ((('const/bool/IN' (A > $o)) e2 s) & (~ (e1 = e2)))) => (('const/pred_set/DISJOINT' A) e1 e2))))) => ((('const/pred_set/CARD' A) (('const/pred_set/BIGUNION' A) s)) = ('const/arithmetic/*' (('const/pred_set/CARD' (A > $o)) s) n))))).
tt('thm/pred_set/BIGINTER_', def, ![A : $t]: (![P : ((A > $o) > $o)]: ((('const/pred_set/BIGINTER' A) P) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s P) => (('const/bool/IN' A) x s))))))))).
tt('thm/pred_set/IN_BIGINTER_', ax, ![A : $t]: (![x : A, B : ((A > $o) > $o)]: ((('const/bool/IN' A) x (('const/pred_set/BIGINTER' A) B)) = (![P : (A > $o)]: ((('const/bool/IN' (A > $o)) P B) => (('const/bool/IN' A) x P)))))).
tt('thm/pred_set/BIGINTER_applied_', ax, ![A : $t]: (![x : A, B : ((A > $o) > $o)]: ((('const/pred_set/BIGINTER' A) B x) = (![P : (A > $o)]: ((('const/bool/IN' (A > $o)) P B) => (('const/bool/IN' A) x P)))))).
tt('thm/pred_set/BIGINTER_INSERT_', ax, ![A : $t]: (![P : (A > $o), B : ((A > $o) > $o)]: ((('const/pred_set/BIGINTER' A) (('const/pred_set/INSERT' (A > $o)) P B)) = (('const/pred_set/INTER' A) P (('const/pred_set/BIGINTER' A) B))))).
tt('thm/pred_set/BIGINTER_EMPTY_', ax, ![A : $t]: ((('const/pred_set/BIGINTER' A) ('const/pred_set/EMPTY' (A > $o))) = ('const/pred_set/UNIV' A))).
tt('thm/pred_set/BIGINTER_INTER_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o)]: ((('const/pred_set/BIGINTER' A) (('const/pred_set/INSERT' (A > $o)) P (('const/pred_set/INSERT' (A > $o)) Q ('const/pred_set/EMPTY' (A > $o))))) = (('const/pred_set/INTER' A) P Q)))).
tt('thm/pred_set/BIGINTER_SING_', ax, ![A : $t]: (![P : (A > $o)]: ((('const/pred_set/BIGINTER' A) (('const/pred_set/INSERT' (A > $o)) P ('const/pred_set/EMPTY' (A > $o)))) = P))).
tt('thm/pred_set/SUBSET_BIGINTER_', ax, ![A : $t]: (![X : (A > $o), P : ((A > $o) > $o)]: ((('const/pred_set/SUBSET' A) X (('const/pred_set/BIGINTER' A) P)) = (![Y : (A > $o)]: ((('const/bool/IN' (A > $o)) Y P) => (('const/pred_set/SUBSET' A) X Y)))))).
tt('thm/pred_set/DISJOINT_BIGINTER_', ax, ![A : $t]: (![X : (A > $o), Y : (A > $o), P : ((A > $o) > $o)]: (((('const/bool/IN' (A > $o)) Y P) & (('const/pred_set/DISJOINT' A) Y X)) => ((('const/pred_set/DISJOINT' A) X (('const/pred_set/BIGINTER' A) P)) & (('const/pred_set/DISJOINT' A) (('const/pred_set/BIGINTER' A) P) X))))).
tt('thm/pred_set/BIGINTER_UNION_', ax, ![A : $t]: (![s1 : ((A > $o) > $o), s2 : ((A > $o) > $o)]: ((('const/pred_set/BIGINTER' A) (('const/pred_set/UNION' (A > $o)) s1 s2)) = (('const/pred_set/INTER' A) (('const/pred_set/BIGINTER' A) s1) (('const/pred_set/BIGINTER' A) s2))))).
tt('thm/pred_set/CROSS_DEF_', def, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o)]: ((('const/pred_set/CROSS' A B) P Q) = (('const/pred_set/GSPEC' ('type/pair/prod' A B) ('type/pair/prod' A B)) (^[p : ('type/pair/prod' A B)]: (('const/pair/,' ('type/pair/prod' A B) $o) p ((('const/bool/IN' A) (('const/pair/FST' A B) p) P) & (('const/bool/IN' B) (('const/pair/SND' A B) p) Q)))))))).
tt('thm/pred_set/IN_CROSS_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o), x : ('type/pair/prod' A B)]: ((('const/bool/IN' ('type/pair/prod' A B)) x (('const/pred_set/CROSS' A B) P Q)) = ((('const/bool/IN' A) (('const/pair/FST' A B) x) P) & (('const/bool/IN' B) (('const/pair/SND' A B) x) Q))))).
tt('thm/pred_set/CROSS_applied_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o), x : ('type/pair/prod' A B)]: ((('const/pred_set/CROSS' A B) P Q x) = ((('const/bool/IN' A) (('const/pair/FST' A B) x) P) & (('const/bool/IN' B) (('const/pair/SND' A B) x) Q))))).
tt('thm/pred_set/CROSS_EMPTY_0', ax, ![A : $t, B : $t]: (![P : (A > $o)]: ((('const/pred_set/CROSS' A B) P ('const/pred_set/EMPTY' B)) = ('const/pred_set/EMPTY' ('type/pair/prod' A B))))).
tt('thm/pred_set/CROSS_EMPTY_e1', ax, ![C : $t, A : $t]: (![P : (A > $o)]: ((('const/pred_set/CROSS' C A) ('const/pred_set/EMPTY' C) P) = ('const/pred_set/EMPTY' ('type/pair/prod' C A))))).
tt('thm/pred_set/CROSS_EMPTY_EQN_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o)]: (((('const/pred_set/CROSS' A B) s t) = ('const/pred_set/EMPTY' ('type/pair/prod' A B))) = ((s = ('const/pred_set/EMPTY' A)) | (t = ('const/pred_set/EMPTY' B)))))).
tt('thm/pred_set/CROSS_INSERT_LEFT_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o), x : A]: ((('const/pred_set/CROSS' A B) (('const/pred_set/INSERT' A) x P) Q) = (('const/pred_set/UNION' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) Q) (('const/pred_set/CROSS' A B) P Q))))).
tt('thm/pred_set/CROSS_INSERT_RIGHT_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o), x : B]: ((('const/pred_set/CROSS' A B) P (('const/pred_set/INSERT' B) x Q)) = (('const/pred_set/UNION' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) P (('const/pred_set/INSERT' B) x ('const/pred_set/EMPTY' B))) (('const/pred_set/CROSS' A B) P Q))))).
tt('thm/pred_set/FINITE_CROSS_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o)]: (((('const/pred_set/FINITE' A) P) & (('const/pred_set/FINITE' B) Q)) => (('const/pred_set/FINITE' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) P Q))))).
tt('thm/pred_set/CROSS_SINGS_', ax, ![A : $t, B : $t]: (![x : A, y : B]: ((('const/pred_set/CROSS' A B) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) (('const/pred_set/INSERT' B) y ('const/pred_set/EMPTY' B))) = (('const/pred_set/INSERT' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/pred_set/EMPTY' ('type/pair/prod' A B)))))).
tt('thm/pred_set/CARD_SING_CROSS_', ax, ![B : $t, A : $t]: (![x : A, P : (B > $o)]: ((('const/pred_set/FINITE' B) P) => ((('const/pred_set/CARD' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) P)) = (('const/pred_set/CARD' B) P))))).
tt('thm/pred_set/CARD_CROSS_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o)]: (((('const/pred_set/FINITE' A) P) & (('const/pred_set/FINITE' B) Q)) => ((('const/pred_set/CARD' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) P Q)) = ('const/arithmetic/*' (('const/pred_set/CARD' A) P) (('const/pred_set/CARD' B) Q)))))).
tt('thm/pred_set/CROSS_SUBSET_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o), P0 : (A > $o), Q0 : (B > $o)]: ((('const/pred_set/SUBSET' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) P0 Q0) (('const/pred_set/CROSS' A B) P Q)) = ((P0 = ('const/pred_set/EMPTY' A)) | ((Q0 = ('const/pred_set/EMPTY' B)) | ((('const/pred_set/SUBSET' A) P0 P) & (('const/pred_set/SUBSET' B) Q0 Q))))))).
tt('thm/pred_set/FINITE_CROSS_EQ_', ax, ![B : $t, A : $t]: (![P : (A > $o), Q : (B > $o)]: ((('const/pred_set/FINITE' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) P Q)) = ((P = ('const/pred_set/EMPTY' A)) | ((Q = ('const/pred_set/EMPTY' B)) | ((('const/pred_set/FINITE' A) P) & (('const/pred_set/FINITE' B) Q))))))).
tt('thm/pred_set/CROSS_UNIV_', ax, ![B : $t, A : $t]: (('const/pred_set/UNIV' ('type/pair/prod' A B)) = (('const/pred_set/CROSS' A B) ('const/pred_set/UNIV' A) ('const/pred_set/UNIV' B)))).
tt('thm/pred_set/INFINITE_PAIR_UNIV_', ax, ![B : $t, A : $t]: ((('const/pred_set/FINITE' ('type/pair/prod' A B)) ('const/pred_set/UNIV' ('type/pair/prod' A B))) = ((('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A)) & (('const/pred_set/FINITE' B) ('const/pred_set/UNIV' B))))).
tt('thm/pred_set/SUM_UNIV_', ax, ![B : $t, A : $t]: (('const/pred_set/UNIV' ('type/sum/sum' A B)) = (('const/pred_set/UNION' ('type/sum/sum' A B)) (('const/pred_set/IMAGE' A ('type/sum/sum' A B)) ('const/sum/INL' A B) ('const/pred_set/UNIV' A)) (('const/pred_set/IMAGE' B ('type/sum/sum' A B)) ('const/sum/INR' A B) ('const/pred_set/UNIV' B))))).
tt('thm/pred_set/INJ_INL_', ax, ![A : $t, B : $t]: (![t : (('type/sum/sum' A B) > $o), s : (A > $o)]: ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' ('type/sum/sum' A B)) (('const/sum/INL' A B) x) t))) => (('const/pred_set/INJ' A ('type/sum/sum' A B)) ('const/sum/INL' A B) s t)))).
tt('thm/pred_set/INJ_INR_', ax, ![B : $t, A : $t]: (![t : (('type/sum/sum' B A) > $o), s : (A > $o)]: ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' ('type/sum/sum' B A)) (('const/sum/INR' B A) x) t))) => (('const/pred_set/INJ' A ('type/sum/sum' B A)) ('const/sum/INR' B A) s t)))).
tt('thm/pred_set/COMPL_DEF_', def, ![A : $t]: (![P : (A > $o)]: ((('const/pred_set/COMPL' A) P) = (('const/pred_set/DIFF' A) ('const/pred_set/UNIV' A) P)))).
tt('thm/pred_set/IN_COMPL_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/bool/IN' A) x (('const/pred_set/COMPL' A) s)) = (~ (('const/bool/IN' A) x s))))).
tt('thm/pred_set/COMPL_applied_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/COMPL' A) s x) = (~ (('const/bool/IN' A) x s))))).
tt('thm/pred_set/COMPL_COMPL_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/COMPL' A) (('const/pred_set/COMPL' A) s)) = s))).
tt('thm/pred_set/COMPL_CLAUSES_0', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/INTER' A) (('const/pred_set/COMPL' A) s) s) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/COMPL_CLAUSES_e1', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/UNION' A) (('const/pred_set/COMPL' A) s) s) = ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/COMPL_SPLITS_', ax, ![A : $t]: (![p : (A > $o), q : (A > $o)]: ((('const/pred_set/UNION' A) (('const/pred_set/INTER' A) p q) (('const/pred_set/INTER' A) (('const/pred_set/COMPL' A) p) q)) = q))).
tt('thm/pred_set/INTER_UNION_COMPL_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/INTER' A) s t) = (('const/pred_set/COMPL' A) (('const/pred_set/UNION' A) (('const/pred_set/COMPL' A) s) (('const/pred_set/COMPL' A) t)))))).
tt('thm/pred_set/COMPL_EMPTY_', ax, ![A : $t]: ((('const/pred_set/COMPL' A) ('const/pred_set/EMPTY' A)) = ('const/pred_set/UNIV' A))).
tt('thm/pred_set/COMPL_INTER_0', ax, ![A : $t]: (![x : (A > $o)]: ((('const/pred_set/INTER' A) x (('const/pred_set/COMPL' A) x)) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/COMPL_INTER_e1', ax, ![A : $t]: (![x : (A > $o)]: ((('const/pred_set/INTER' A) (('const/pred_set/COMPL' A) x) x) = ('const/pred_set/EMPTY' A)))).
tt('thm/pred_set/COMPL_UNION_', ax, ![A : $t]: (![t : (A > $o), s : (A > $o)]: ((('const/pred_set/COMPL' A) (('const/pred_set/UNION' A) s t)) = (('const/pred_set/INTER' A) (('const/pred_set/COMPL' A) s) (('const/pred_set/COMPL' A) t))))).
tt('thm/pred_set/count_def_', def, (![n : 'type/num/num']: (('const/pred_set/count' n) = (('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[m : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) m ('const/prim_rec/<' m n))))))).
tt('thm/pred_set/IN_COUNT_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/bool/IN' 'type/num/num') m ('const/pred_set/count' n)) = ('const/prim_rec/<' m n)))).
tt('thm/pred_set/COUNT_applied_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/pred_set/count' n m) = ('const/prim_rec/<' m n)))).
tt('thm/pred_set/COUNT_ZERO_', ax, (('const/pred_set/count' 'const/num/0') = ('const/pred_set/EMPTY' 'type/num/num'))).
tt('thm/pred_set/COUNT_SUC_', ax, (![n : 'type/num/num']: (('const/pred_set/count' ('const/num/SUC' n)) = (('const/pred_set/INSERT' 'type/num/num') n ('const/pred_set/count' n))))).
tt('thm/pred_set/FINITE_COUNT_', ax, (![n : 'type/num/num']: (('const/pred_set/FINITE' 'type/num/num') ('const/pred_set/count' n)))).
tt('thm/pred_set/CARD_COUNT_', ax, (![n : 'type/num/num']: ((('const/pred_set/CARD' 'type/num/num') ('const/pred_set/count' n)) = n))).
tt('thm/pred_set/COUNT_11_', ax, (![n2 : 'type/num/num', n1 : 'type/num/num']: ((('const/pred_set/count' n1) = ('const/pred_set/count' n2)) = (n1 = n2)))).
tt('thm/pred_set/ITSET_tupled_primitive_def_', def, ![B : $t, A : $t]: (![f : (A > (B > B))]: ((('const/pred_set/ITSET_tupled' A B) f) = (('const/relation/WFREC' ('type/pair/prod' (A > $o) B) B) (('const/min/@' (('type/pair/prod' (A > $o) B) > (('type/pair/prod' (A > $o) B) > $o))) (^[R : (('type/pair/prod' (A > $o) B) > (('type/pair/prod' (A > $o) B) > $o))]: ((('const/relation/WF' ('type/pair/prod' (A > $o) B)) R) & (![b : B, s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (~ (s = ('const/pred_set/EMPTY' A)))) => (R (('const/pair/,' (A > $o) B) (('const/pred_set/REST' A) s) (f (('const/pred_set/CHOICE' A) s) b)) (('const/pair/,' (A > $o) B) s b))))))) (^[ITSET_tupled : (('type/pair/prod' (A > $o) B) > B), a : ('type/pair/prod' (A > $o) B)]: (('const/pair/pair_CASE' B (A > $o) B) a (^[s : (A > $o), b : B]: (('const/combin/I' B) (('const/bool/COND' B) (('const/pred_set/FINITE' A) s) (('const/bool/COND' B) (s = ('const/pred_set/EMPTY' A)) b (ITSET_tupled (('const/pair/,' (A > $o) B) (('const/pred_set/REST' A) s) (f (('const/pred_set/CHOICE' A) s) b)))) ('const/bool/ARB' B)))))))))).
tt('thm/pred_set/ITSET_curried_def_', def, ![B : $t, A : $t]: (![f : (A > (B > B)), x : (A > $o), x1 : B]: ((('const/pred_set/ITSET' A B) f x x1) = (('const/pred_set/ITSET_tupled' A B) f (('const/pair/,' (A > $o) B) x x1))))).
tt('thm/pred_set/ITSET_ind_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), P : ((A > $o) > (B > $o))]: ((![s : (A > $o), b : B]: ((((('const/pred_set/FINITE' A) s) & (~ (s = ('const/pred_set/EMPTY' A)))) => (P (('const/pred_set/REST' A) s) (f (('const/pred_set/CHOICE' A) s) b))) => (P s b))) => (![v : (A > $o), v1 : B]: (P v v1))))).
tt('thm/pred_set/ITSET_def_', ax, ![B : $t, A : $t]: (![s : (A > $o), f : (A > (B > B)), b : B]: ((('const/pred_set/ITSET' A B) f s b) = (('const/bool/COND' B) (('const/pred_set/FINITE' A) s) (('const/bool/COND' B) (s = ('const/pred_set/EMPTY' A)) b (('const/pred_set/ITSET' A B) f (('const/pred_set/REST' A) s) (f (('const/pred_set/CHOICE' A) s) b))) ('const/bool/ARB' B))))).
tt('thm/pred_set/ITSET_IND_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), P : ((A > $o) > (B > $o))]: ((![s : (A > $o), b : B]: ((((('const/pred_set/FINITE' A) s) & (~ (s = ('const/pred_set/EMPTY' A)))) => (P (('const/pred_set/REST' A) s) (f (('const/pred_set/CHOICE' A) s) b))) => (P s b))) => (![v : (A > $o), v1 : B]: (P v v1))))).
tt('thm/pred_set/ITSET_THM_', ax, ![B : $t, A : $t]: (![s : (A > $o), f : (A > (B > B)), b : B]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/ITSET' A B) f s b) = (('const/bool/COND' B) (s = ('const/pred_set/EMPTY' A)) b (('const/pred_set/ITSET' A B) f (('const/pred_set/REST' A) s) (f (('const/pred_set/CHOICE' A) s) b))))))).
tt('thm/pred_set/ITSET_EMPTY_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), b : B]: ((('const/pred_set/ITSET' A B) f ('const/pred_set/EMPTY' A) b) = b))).
tt('thm/pred_set/ITSET_INSERT_', ax, ![B : $t, A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > (B > B)), x : A, b : B]: ((('const/pred_set/ITSET' A B) f (('const/pred_set/INSERT' A) x s) b) = (('const/pred_set/ITSET' A B) f (('const/pred_set/REST' A) (('const/pred_set/INSERT' A) x s)) (f (('const/pred_set/CHOICE' A) (('const/pred_set/INSERT' A) x s)) b))))))).
tt('thm/pred_set/COMMUTING_ITSET_INSERT_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), s : (A > $o)]: (((![x : A, y : A, z : B]: ((f x (f y z)) = (f y (f x z)))) & (('const/pred_set/FINITE' A) s)) => (![x : A, b : B]: ((('const/pred_set/ITSET' A B) f (('const/pred_set/INSERT' A) x s) b) = (('const/pred_set/ITSET' A B) f (('const/pred_set/DELETE' A) s x) (f x b))))))).
tt('thm/pred_set/COMMUTING_ITSET_RECURSES_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), e : A, s : (A > $o), b : B]: (((![x : A, y : A, z : B]: ((f x (f y z)) = (f y (f x z)))) & (('const/pred_set/FINITE' A) s)) => ((('const/pred_set/ITSET' A B) f (('const/pred_set/INSERT' A) e s) b) = (f e (('const/pred_set/ITSET' A B) f (('const/pred_set/DELETE' A) s e) b)))))).
tt('thm/pred_set/SUM_IMAGE_DEF_', def, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/SUM_IMAGE' A) f s) = (('const/pred_set/ITSET' A 'type/num/num') (^[e : A, acc : 'type/num/num']: ('const/arithmetic/+' (f e) acc)) s 'const/num/0')))).
tt('thm/pred_set/SUM_IMAGE_THM_0', ax, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/pred_set/SUM_IMAGE' A) f ('const/pred_set/EMPTY' A)) = 'const/num/0'))).
tt('thm/pred_set/SUM_IMAGE_THM_e1', ax, ![A : $t]: (![f : (A > 'type/num/num'), e : A, s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/SUM_IMAGE' A) f (('const/pred_set/INSERT' A) e s)) = ('const/arithmetic/+' (f e) (('const/pred_set/SUM_IMAGE' A) f (('const/pred_set/DELETE' A) s e))))))).
tt('thm/pred_set/SUM_IMAGE_SING_', ax, ![A : $t]: (![f : (A > 'type/num/num'), e : A]: ((('const/pred_set/SUM_IMAGE' A) f (('const/pred_set/INSERT' A) e ('const/pred_set/EMPTY' A))) = (f e)))).
tt('thm/pred_set/SUM_IMAGE_SUBSET_LE_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o), t : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (('const/pred_set/SUBSET' A) t s)) => ('const/arithmetic/<=' (('const/pred_set/SUM_IMAGE' A) f t) (('const/pred_set/SUM_IMAGE' A) f s))))).
tt('thm/pred_set/SUM_IMAGE_IN_LE_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o), e : A]: (((('const/pred_set/FINITE' A) s) & (('const/bool/IN' A) e s)) => ('const/arithmetic/<=' (f e) (('const/pred_set/SUM_IMAGE' A) f s))))).
tt('thm/pred_set/SUM_IMAGE_DELETE_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![e : A]: ((('const/pred_set/SUM_IMAGE' A) f (('const/pred_set/DELETE' A) s e)) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' A) e s) ('const/arithmetic/-' (('const/pred_set/SUM_IMAGE' A) f s) (f e)) (('const/pred_set/SUM_IMAGE' A) f s))))))).
tt('thm/pred_set/SUM_IMAGE_UNION_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o), t : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (('const/pred_set/FINITE' A) t)) => ((('const/pred_set/SUM_IMAGE' A) f (('const/pred_set/UNION' A) s t)) = ('const/arithmetic/-' ('const/arithmetic/+' (('const/pred_set/SUM_IMAGE' A) f s) (('const/pred_set/SUM_IMAGE' A) f t)) (('const/pred_set/SUM_IMAGE' A) f (('const/pred_set/INTER' A) s t))))))).
tt('thm/pred_set/SUM_IMAGE_lower_bound_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![n : 'type/num/num']: ((![x : A]: ((('const/bool/IN' A) x s) => ('const/arithmetic/<=' n (f x)))) => ('const/arithmetic/<=' ('const/arithmetic/*' (('const/pred_set/CARD' A) s) n) (('const/pred_set/SUM_IMAGE' A) f s))))))).
tt('thm/pred_set/SUM_IMAGE_upper_bound_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![n : 'type/num/num']: ((![x : A]: ((('const/bool/IN' A) x s) => ('const/arithmetic/<=' (f x) n))) => ('const/arithmetic/<=' (('const/pred_set/SUM_IMAGE' A) f s) ('const/arithmetic/*' (('const/pred_set/CARD' A) s) n))))))).
tt('thm/pred_set/SUM_SAME_IMAGE_', ax, ![A : $t]: (![P : (A > $o)]: ((('const/pred_set/FINITE' A) P) => (![f : (A > 'type/num/num'), p : A]: (((('const/bool/IN' A) p P) & (![q : A]: ((('const/bool/IN' A) q P) => ((f p) = (f q))))) => ((('const/pred_set/SUM_IMAGE' A) f P) = ('const/arithmetic/*' (('const/pred_set/CARD' A) P) (f p)))))))).
tt('thm/pred_set/SUM_IMAGE_CONG_', ax, ![A : $t]: (![s2 : (A > $o), s1 : (A > $o), f2 : (A > 'type/num/num'), f1 : (A > 'type/num/num')]: (((s1 = s2) & (![x : A]: ((('const/bool/IN' A) x s2) => ((f1 x) = (f2 x))))) => ((('const/pred_set/SUM_IMAGE' A) f1 s1) = (('const/pred_set/SUM_IMAGE' A) f2 s2))))).
tt('thm/pred_set/SUM_IMAGE_ZERO_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (((('const/pred_set/SUM_IMAGE' A) f s) = 'const/num/0') = (![x : A]: ((('const/bool/IN' A) x s) => ((f x) = 'const/num/0'))))))).
tt('thm/pred_set/ABS_DIFF_SUM_IMAGE_', ax, ![A : $t]: (![g : (A > 'type/num/num'), f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ('const/arithmetic/<=' ('const/arithmetic/ABS_DIFF' (('const/pred_set/SUM_IMAGE' A) f s) (('const/pred_set/SUM_IMAGE' A) g s)) (('const/pred_set/SUM_IMAGE' A) (^[x : A]: ('const/arithmetic/ABS_DIFF' (f x) (g x))) s))))).
tt('thm/pred_set/SUM_IMAGE_MONO_LESS_EQ_', ax, ![A : $t]: (![g : (A > 'type/num/num'), f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((![x : A]: ((('const/bool/IN' A) x s) => ('const/arithmetic/<=' (f x) (g x)))) => ('const/arithmetic/<=' (('const/pred_set/SUM_IMAGE' A) f s) (('const/pred_set/SUM_IMAGE' A) g s)))))).
tt('thm/pred_set/SUM_IMAGE_MONO_LESS_', ax, ![A : $t]: (![g : (A > 'type/num/num'), f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (((?[x : A]: ((('const/bool/IN' A) x s) & ('const/prim_rec/<' (f x) (g x)))) & (![x : A]: ((('const/bool/IN' A) x s) => ('const/arithmetic/<=' (f x) (g x))))) => ('const/prim_rec/<' (('const/pred_set/SUM_IMAGE' A) f s) (('const/pred_set/SUM_IMAGE' A) g s)))))).
tt('thm/pred_set/SUM_SET_DEF_', def, ('const/pred_set/SUM_SET' = (('const/pred_set/SUM_IMAGE' 'type/num/num') ('const/combin/I' 'type/num/num')))).
tt('thm/pred_set/SUM_SET_THM_0', ax, (('const/pred_set/SUM_SET' ('const/pred_set/EMPTY' 'type/num/num')) = 'const/num/0')).
tt('thm/pred_set/SUM_SET_THM_e1', ax, (![x : 'type/num/num', s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (('const/pred_set/SUM_SET' (('const/pred_set/INSERT' 'type/num/num') x s)) = ('const/arithmetic/+' x ('const/pred_set/SUM_SET' (('const/pred_set/DELETE' 'type/num/num') s x))))))).
tt('thm/pred_set/SUM_SET_EMPTY_', ax, (('const/pred_set/SUM_SET' ('const/pred_set/EMPTY' 'type/num/num')) = 'const/num/0')).
tt('thm/pred_set/SUM_SET_SING_', ax, (![n : 'type/num/num']: (('const/pred_set/SUM_SET' (('const/pred_set/INSERT' 'type/num/num') n ('const/pred_set/EMPTY' 'type/num/num'))) = n))).
tt('thm/pred_set/SUM_SET_SUBSET_LE_', ax, (![s : ('type/num/num' > $o), t : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') t) & (('const/pred_set/SUBSET' 'type/num/num') s t)) => ('const/arithmetic/<=' ('const/pred_set/SUM_SET' s) ('const/pred_set/SUM_SET' t))))).
tt('thm/pred_set/SUM_SET_IN_LE_', ax, (![x : 'type/num/num', s : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') s) & (('const/bool/IN' 'type/num/num') x s)) => ('const/arithmetic/<=' x ('const/pred_set/SUM_SET' s))))).
tt('thm/pred_set/SUM_SET_DELETE_', ax, (![s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (![e : 'type/num/num']: (('const/pred_set/SUM_SET' (('const/pred_set/DELETE' 'type/num/num') s e)) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' 'type/num/num') e s) ('const/arithmetic/-' ('const/pred_set/SUM_SET' s) e) ('const/pred_set/SUM_SET' s))))))).
tt('thm/pred_set/SUM_SET_UNION_', ax, (![s : ('type/num/num' > $o), t : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') s) & (('const/pred_set/FINITE' 'type/num/num') t)) => (('const/pred_set/SUM_SET' (('const/pred_set/UNION' 'type/num/num') s t)) = ('const/arithmetic/-' ('const/arithmetic/+' ('const/pred_set/SUM_SET' s) ('const/pred_set/SUM_SET' t)) ('const/pred_set/SUM_SET' (('const/pred_set/INTER' 'type/num/num') s t))))))).
tt('thm/pred_set/PROD_IMAGE_DEF_', def, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/pred_set/PROD_IMAGE' A) f s) = (('const/pred_set/ITSET' A 'type/num/num') (^[e : A, acc : 'type/num/num']: ('const/arithmetic/*' (f e) acc)) s ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/pred_set/PROD_IMAGE_THM_0', ax, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/pred_set/PROD_IMAGE' A) f ('const/pred_set/EMPTY' A)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/pred_set/PROD_IMAGE_THM_e1', ax, ![A : $t]: (![f : (A > 'type/num/num'), e : A, s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/PROD_IMAGE' A) f (('const/pred_set/INSERT' A) e s)) = ('const/arithmetic/*' (f e) (('const/pred_set/PROD_IMAGE' A) f (('const/pred_set/DELETE' A) s e))))))).
tt('thm/pred_set/PROD_SET_DEF_', def, ('const/pred_set/PROD_SET' = (('const/pred_set/PROD_IMAGE' 'type/num/num') ('const/combin/I' 'type/num/num')))).
tt('thm/pred_set/PROD_SET_THM_0', ax, (('const/pred_set/PROD_SET' ('const/pred_set/EMPTY' 'type/num/num')) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/pred_set/PROD_SET_THM_e1', ax, (![x : 'type/num/num', s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (('const/pred_set/PROD_SET' (('const/pred_set/INSERT' 'type/num/num') x s)) = ('const/arithmetic/*' x ('const/pred_set/PROD_SET' (('const/pred_set/DELETE' 'type/num/num') s x))))))).
tt('thm/pred_set/PROD_SET_EMPTY_', ax, (('const/pred_set/PROD_SET' ('const/pred_set/EMPTY' 'type/num/num')) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/pred_set/PROD_SET_IMAGE_REDUCTION_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o), x : A]: (((('const/pred_set/FINITE' 'type/num/num') (('const/pred_set/IMAGE' A 'type/num/num') f s)) & (~ (('const/bool/IN' 'type/num/num') (f x) (('const/pred_set/IMAGE' A 'type/num/num') f s)))) => (('const/pred_set/PROD_SET' (('const/pred_set/IMAGE' A 'type/num/num') f (('const/pred_set/INSERT' A) x s))) = ('const/arithmetic/*' (f x) ('const/pred_set/PROD_SET' (('const/pred_set/IMAGE' A 'type/num/num') f s))))))).
tt('thm/pred_set/MAX_SET_DEF_', def, (![s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (((~ (s = ('const/pred_set/EMPTY' 'type/num/num'))) => ((('const/bool/IN' 'type/num/num') ('const/pred_set/MAX_SET' s) s) & (![y : 'type/num/num']: ((('const/bool/IN' 'type/num/num') y s) => ('const/arithmetic/<=' y ('const/pred_set/MAX_SET' s)))))) & ((s = ('const/pred_set/EMPTY' 'type/num/num')) => (('const/pred_set/MAX_SET' s) = 'const/num/0')))))).
tt('thm/pred_set/MAX_SET_THM_0', ax, (('const/pred_set/MAX_SET' ('const/pred_set/EMPTY' 'type/num/num')) = 'const/num/0')).
tt('thm/pred_set/MAX_SET_THM_e1', ax, (![e : 'type/num/num', s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (('const/pred_set/MAX_SET' (('const/pred_set/INSERT' 'type/num/num') e s)) = ('const/arithmetic/MAX' e ('const/pred_set/MAX_SET' s)))))).
tt('thm/pred_set/MAX_SET_REWRITES_0', ax, (('const/pred_set/MAX_SET' ('const/pred_set/EMPTY' 'type/num/num')) = 'const/num/0')).
tt('thm/pred_set/MAX_SET_REWRITES_e1', ax, (![e : 'type/num/num']: (('const/pred_set/MAX_SET' (('const/pred_set/INSERT' 'type/num/num') e ('const/pred_set/EMPTY' 'type/num/num'))) = e))).
tt('thm/pred_set/MAX_SET_ELIM_', ax, (![P : ('type/num/num' > $o), Q : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') P) & (((P = ('const/pred_set/EMPTY' 'type/num/num')) => (Q 'const/num/0')) & (![x : 'type/num/num']: (((![y : 'type/num/num']: ((('const/bool/IN' 'type/num/num') y P) => ('const/arithmetic/<=' y x))) & (('const/bool/IN' 'type/num/num') x P)) => (Q x))))) => (Q ('const/pred_set/MAX_SET' P))))).
tt('thm/pred_set/MIN_SET_DEF_', def, ('const/pred_set/MIN_SET' = 'const/while/LEAST')).
tt('thm/pred_set/MIN_SET_ELIM_', ax, (![P : ('type/num/num' > $o), Q : ('type/num/num' > $o)]: (((~ (P = ('const/pred_set/EMPTY' 'type/num/num'))) & (![x : 'type/num/num']: (((![y : 'type/num/num']: ((('const/bool/IN' 'type/num/num') y P) => ('const/arithmetic/<=' x y))) & (('const/bool/IN' 'type/num/num') x P)) => (Q x)))) => (Q ('const/pred_set/MIN_SET' P))))).
tt('thm/pred_set/MIN_SET_THM_0', ax, (![e : 'type/num/num']: (('const/pred_set/MIN_SET' (('const/pred_set/INSERT' 'type/num/num') e ('const/pred_set/EMPTY' 'type/num/num'))) = e))).
tt('thm/pred_set/MIN_SET_THM_e1', ax, (![s : ('type/num/num' > $o), e1 : 'type/num/num', e2 : 'type/num/num']: (('const/pred_set/MIN_SET' (('const/pred_set/INSERT' 'type/num/num') e1 (('const/pred_set/INSERT' 'type/num/num') e2 s))) = ('const/arithmetic/MIN' e1 ('const/pred_set/MIN_SET' (('const/pred_set/INSERT' 'type/num/num') e2 s)))))).
tt('thm/pred_set/MIN_SET_LEM_', ax, (![s : ('type/num/num' > $o)]: ((~ (s = ('const/pred_set/EMPTY' 'type/num/num'))) => ((('const/bool/IN' 'type/num/num') ('const/pred_set/MIN_SET' s) s) & (![x : 'type/num/num']: ((('const/bool/IN' 'type/num/num') x s) => ('const/arithmetic/<=' ('const/pred_set/MIN_SET' s) x))))))).
tt('thm/pred_set/SUBSET_MIN_SET_', ax, ![A : $t]: (![I : ('type/num/num' > $o), J : ('type/num/num' > $o), n : A]: (((~ (I = ('const/pred_set/EMPTY' 'type/num/num'))) & ((~ (J = ('const/pred_set/EMPTY' 'type/num/num'))) & (('const/pred_set/SUBSET' 'type/num/num') I J))) => ('const/arithmetic/<=' ('const/pred_set/MIN_SET' J) ('const/pred_set/MIN_SET' I))))).
tt('thm/pred_set/SUBSET_MAX_SET_', ax, ![A : $t]: (![I : ('type/num/num' > $o), J : ('type/num/num' > $o), n : A]: (((('const/pred_set/FINITE' 'type/num/num') I) & ((('const/pred_set/FINITE' 'type/num/num') J) & (('const/pred_set/SUBSET' 'type/num/num') I J))) => ('const/arithmetic/<=' ('const/pred_set/MAX_SET' I) ('const/pred_set/MAX_SET' J))))).
tt('thm/pred_set/MIN_SET_LEQ_MAX_SET_', ax, (![s : ('type/num/num' > $o)]: (((~ (s = ('const/pred_set/EMPTY' 'type/num/num'))) & (('const/pred_set/FINITE' 'type/num/num') s)) => ('const/arithmetic/<=' ('const/pred_set/MIN_SET' s) ('const/pred_set/MAX_SET' s))))).
tt('thm/pred_set/MIN_SET_UNION_', ax, (![A : ('type/num/num' > $o), B : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') A) & ((('const/pred_set/FINITE' 'type/num/num') B) & ((~ (A = ('const/pred_set/EMPTY' 'type/num/num'))) & (~ (B = ('const/pred_set/EMPTY' 'type/num/num')))))) => (('const/pred_set/MIN_SET' (('const/pred_set/UNION' 'type/num/num') A B)) = ('const/arithmetic/MIN' ('const/pred_set/MIN_SET' A) ('const/pred_set/MIN_SET' B)))))).
tt('thm/pred_set/MAX_SET_UNION_', ax, (![A : ('type/num/num' > $o), B : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') A) & (('const/pred_set/FINITE' 'type/num/num') B)) => (('const/pred_set/MAX_SET' (('const/pred_set/UNION' 'type/num/num') A B)) = ('const/arithmetic/MAX' ('const/pred_set/MAX_SET' A) ('const/pred_set/MAX_SET' B)))))).
tt('thm/pred_set/POW_DEF_', def, ![A : $t]: (![set : (A > $o)]: ((('const/pred_set/POW' A) set) = (('const/pred_set/GSPEC' (A > $o) (A > $o)) (^[s : (A > $o)]: (('const/pair/,' (A > $o) $o) s (('const/pred_set/SUBSET' A) s set))))))).
tt('thm/pred_set/IN_POW_', ax, ![A : $t]: (![set : (A > $o), e : (A > $o)]: ((('const/bool/IN' (A > $o)) e (('const/pred_set/POW' A) set)) = (('const/pred_set/SUBSET' A) e set)))).
tt('thm/pred_set/UNIV_FUN_TO_BOOL_', ax, ![A : $t]: (('const/pred_set/UNIV' (A > $o)) = (('const/pred_set/POW' A) ('const/pred_set/UNIV' A)))).
tt('thm/pred_set/SUBSET_POW_', ax, ![A : $t]: (![s1 : (A > $o), s2 : (A > $o)]: ((('const/pred_set/SUBSET' A) s1 s2) => (('const/pred_set/SUBSET' (A > $o)) (('const/pred_set/POW' A) s1) (('const/pred_set/POW' A) s2))))).
tt('thm/pred_set/SUBSET_INSERT_RIGHT_', ax, ![A : $t]: (![e : A, s1 : (A > $o), s2 : (A > $o)]: ((('const/pred_set/SUBSET' A) s1 s2) => (('const/pred_set/SUBSET' A) s1 (('const/pred_set/INSERT' A) e s2))))).
tt('thm/pred_set/SUBSET_DELETE_BOTH_', ax, ![A : $t]: (![s1 : (A > $o), s2 : (A > $o), x : A]: ((('const/pred_set/SUBSET' A) s1 s2) => (('const/pred_set/SUBSET' A) (('const/pred_set/DELETE' A) s1 x) (('const/pred_set/DELETE' A) s2 x))))).
tt('thm/pred_set/POW_EMPTY_', ax, ![A : $t]: (![s : (A > $o)]: (~ ((('const/pred_set/POW' A) s) = ('const/pred_set/EMPTY' (A > $o)))))).
tt('thm/pred_set/POW_INSERT_', ax, ![A : $t]: (![e : A, s : (A > $o)]: ((('const/pred_set/POW' A) (('const/pred_set/INSERT' A) e s)) = (('const/pred_set/UNION' (A > $o)) (('const/pred_set/IMAGE' (A > $o) (A > $o)) (('const/pred_set/INSERT' A) e) (('const/pred_set/POW' A) s)) (('const/pred_set/POW' A) s))))).
tt('thm/pred_set/POW_EQNS_0', ax, ![A : $t]: ((('const/pred_set/POW' A) ('const/pred_set/EMPTY' A)) = (('const/pred_set/INSERT' (A > $o)) ('const/pred_set/EMPTY' A) ('const/pred_set/EMPTY' (A > $o))))).
tt('thm/pred_set/POW_EQNS_e1', ax, ![A : $t]: (![e : A, s : (A > $o)]: ((('const/pred_set/POW' A) (('const/pred_set/INSERT' A) e s)) = (('const/bool/LET' ((A > $o) > $o) ((A > $o) > $o)) (^[ps : ((A > $o) > $o)]: (('const/pred_set/UNION' (A > $o)) (('const/pred_set/IMAGE' (A > $o) (A > $o)) (('const/pred_set/INSERT' A) e) ps) ps)) (('const/pred_set/POW' A) s))))).
tt('thm/pred_set/FINITE_POW_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (('const/pred_set/FINITE' (A > $o)) (('const/pred_set/POW' A) s))))).
tt('thm/pred_set/CARD_POW_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/CARD' (A > $o)) (('const/pred_set/POW' A) s)) = ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/pred_set/CARD' A) s)))))).
tt('thm/pred_set/GSPEC_ETA_', ax, ![A : $t]: (![P : (A > $o)]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (P x)))) = P))).
tt('thm/pred_set/GSPEC_F_', ax, ![A : $t]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x $false))) = ('const/pred_set/EMPTY' A))).
tt('thm/pred_set/GSPEC_T_', ax, ![A : $t]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x $true))) = ('const/pred_set/UNIV' A))).
tt('thm/pred_set/GSPEC_ID_', ax, ![A : $t]: (![y : (A > $o)]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' A) x y)))) = y))).
tt('thm/pred_set/GSPEC_EQ_', ax, ![A : $t]: (![y : A]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (x = y)))) = (('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/GSPEC_EQ2_', ax, ![A : $t]: (![y : A]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (y = x)))) = (('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/GSPEC_F_COND_', ax, ![B : $t, A : $t]: (![f : (A > ('type/pair/prod' B $o))]: ((![x : A]: (~ (('const/pair/SND' B $o) (f x)))) => ((('const/pred_set/GSPEC' B A) f) = ('const/pred_set/EMPTY' B))))).
tt('thm/pred_set/GSPEC_AND_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o)]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((P x) & (Q x))))) = (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (P x)))) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (Q x)))))))).
tt('thm/pred_set/GSPEC_OR_', ax, ![A : $t]: (![P : (A > $o), Q : (A > $o)]: ((('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((P x) | (Q x))))) = (('const/pred_set/UNION' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (P x)))) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (Q x)))))))).
tt('thm/pred_set/equiv_on_def_', def, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: ((('const/pred_set/equiv_on' A) R s) = ((![x : A]: ((('const/bool/IN' A) x s) => (R x x))) & ((![x : A, y : A]: (((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)) => ((R x y) = (R y x)))) & (![x : A, y : A, z : A]: (((('const/bool/IN' A) x s) & ((('const/bool/IN' A) y s) & ((('const/bool/IN' A) z s) & ((R x y) & (R y z))))) => (R x z)))))))).
tt('thm/pred_set/partition_def_', def, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: ((('const/pred_set/partition' A) R s) = (('const/pred_set/GSPEC' (A > $o) (A > $o)) (^[t : (A > $o)]: (('const/pair/,' (A > $o) $o) t (?[x : A]: ((('const/bool/IN' A) x s) & (t = (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((('const/bool/IN' A) y s) & (R x y)))))))))))))).
tt('thm/pred_set/BIGUNION_partition_', ax, ![A : $t]: (![s : (A > $o), R : (A > (A > $o))]: ((('const/pred_set/equiv_on' A) R s) => ((('const/pred_set/BIGUNION' A) (('const/pred_set/partition' A) R s)) = s)))).
tt('thm/pred_set/EMPTY_NOT_IN_partition_', ax, ![A : $t]: (![s : (A > $o), R : (A > (A > $o))]: ((('const/pred_set/equiv_on' A) R s) => (~ (('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/pred_set/partition' A) R s)))))).
tt('thm/pred_set/partition_elements_disjoint_', ax, ![A : $t]: (![s : (A > $o), R : (A > (A > $o))]: ((('const/pred_set/equiv_on' A) R s) => (![t1 : (A > $o), t2 : (A > $o)]: (((('const/bool/IN' (A > $o)) t1 (('const/pred_set/partition' A) R s)) & ((('const/bool/IN' (A > $o)) t2 (('const/pred_set/partition' A) R s)) & (~ (t1 = t2)))) => (('const/pred_set/DISJOINT' A) t1 t2)))))).
tt('thm/pred_set/partition_elements_interrelate_', ax, ![A : $t]: (![s : (A > $o), R : (A > (A > $o))]: ((('const/pred_set/equiv_on' A) R s) => (![t : (A > $o)]: ((('const/bool/IN' (A > $o)) t (('const/pred_set/partition' A) R s)) => (![x : A, y : A]: (((('const/bool/IN' A) x t) & (('const/bool/IN' A) y t)) => (R x y)))))))).
tt('thm/pred_set/partition_SUBSET_', ax, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o), t : (A > $o)]: ((('const/bool/IN' (A > $o)) t (('const/pred_set/partition' A) R s)) => (('const/pred_set/SUBSET' A) t s)))).
tt('thm/pred_set/FINITE_partition_', ax, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/pred_set/FINITE' (A > $o)) (('const/pred_set/partition' A) R s)) & (![t : (A > $o)]: ((('const/bool/IN' (A > $o)) t (('const/pred_set/partition' A) R s)) => (('const/pred_set/FINITE' A) t))))))).
tt('thm/pred_set/partition_CARD_', ax, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: (((('const/pred_set/equiv_on' A) R s) & (('const/pred_set/FINITE' A) s)) => ((('const/pred_set/CARD' A) s) = (('const/pred_set/SUM_IMAGE' (A > $o)) ('const/pred_set/CARD' A) (('const/pred_set/partition' A) R s)))))).
tt('thm/pred_set/pairwise_def_', def, ![A : $t]: (![P : (A > (A > $o)), s : (A > $o)]: ((('const/pred_set/pairwise' A) P s) = (![e1 : A, e2 : A]: (((('const/bool/IN' A) e1 s) & (('const/bool/IN' A) e2 s)) => (P e1 e2)))))).
tt('thm/pred_set/pairwise_UNION_', ax, ![A : $t]: (![s2 : (A > $o), s1 : (A > $o), R : (A > (A > $o))]: ((('const/pred_set/pairwise' A) R (('const/pred_set/UNION' A) s1 s2)) = ((('const/pred_set/pairwise' A) R s1) & ((('const/pred_set/pairwise' A) R s2) & (![x : A, y : A]: (((('const/bool/IN' A) x s1) & (('const/bool/IN' A) y s2)) => ((R x y) & (R y x))))))))).
tt('thm/pred_set/pairwise_SUBSET_', ax, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o), t : (A > $o)]: (((('const/pred_set/pairwise' A) R t) & (('const/pred_set/SUBSET' A) s t)) => (('const/pred_set/pairwise' A) R s)))).
tt('thm/pred_set/KoenigsLemma_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((![x : A]: (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (R x y)))))) => (![x : A]: ((~ (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (('const/relation/RTC' A) R x y)))))) => (?[f : ('type/num/num' > A)]: (((f 'const/num/0') = x) & (![n : 'type/num/num']: (R (f n) (f ('const/num/SUC' n))))))))))).
tt('thm/pred_set/KoenigsLemma_WF_', ax, ![A : $t]: (![R : (A > (A > $o))]: (((![x : A]: (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (R x y)))))) & (('const/relation/WF' A) (('const/relation/inv' A) R))) => (![x : A]: (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (('const/relation/RTC' A) R x y))))))))).
tt('thm/pred_set/SET_EQ_SUBSET_', ax, ![A : $t]: (![s1 : (A > $o), s2 : (A > $o)]: ((s1 = s2) = ((('const/pred_set/SUBSET' A) s1 s2) & (('const/pred_set/SUBSET' A) s2 s1))))).
tt('thm/pred_set/PSUBSET_EQN_', ax, ![A : $t]: (![s1 : (A > $o), s2 : (A > $o)]: ((('const/pred_set/PSUBSET' A) s1 s2) = ((('const/pred_set/SUBSET' A) s1 s2) & (~ (('const/pred_set/SUBSET' A) s2 s1)))))).
tt('thm/pred_set/PSUBSET_SUBSET_TRANS_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/pred_set/PSUBSET' A) s t) & (('const/pred_set/SUBSET' A) t u)) => (('const/pred_set/PSUBSET' A) s u)))).
tt('thm/pred_set/SUBSET_PSUBSET_TRANS_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/pred_set/SUBSET' A) s t) & (('const/pred_set/PSUBSET' A) t u)) => (('const/pred_set/PSUBSET' A) s u)))).
tt('thm/pred_set/CROSS_EQNS_0', ax, ![A : $t, B : $t]: (![s2 : (B > $o)]: ((('const/pred_set/CROSS' A B) ('const/pred_set/EMPTY' A) s2) = ('const/pred_set/EMPTY' ('type/pair/prod' A B))))).
tt('thm/pred_set/CROSS_EQNS_e1', ax, ![B : $t, A : $t]: (![s2 : (B > $o), s1 : (A > $o), a : A]: ((('const/pred_set/CROSS' A B) (('const/pred_set/INSERT' A) a s1) s2) = (('const/pred_set/UNION' ('type/pair/prod' A B)) (('const/pred_set/IMAGE' B ('type/pair/prod' A B)) (^[y : B]: (('const/pair/,' A B) a y)) s2) (('const/pred_set/CROSS' A B) s1 s2))))).
tt('thm/pred_set/count_EQN_', ax, (![n : 'type/num/num']: (('const/pred_set/count' n) = (('const/bool/COND' ('type/num/num' > $o)) (n = 'const/num/0') ('const/pred_set/EMPTY' 'type/num/num') (('const/bool/LET' 'type/num/num' ('type/num/num' > $o)) (^[p : 'type/num/num']: (('const/pred_set/INSERT' 'type/num/num') p ('const/pred_set/count' p))) ('const/prim_rec/PRE' n)))))).
tt('thm/pred_set/UNIQUE_MEMBER_SING_', ax, ![A : $t]: (![x : A, s : (A > $o)]: (((('const/bool/IN' A) x s) & (![y : A]: ((('const/bool/IN' A) y s) => (x = y)))) = (s = (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))))).
tt('thm/pred_set/inj_surj_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: ((('const/pred_set/INJ' A B) f s t) => ((s = ('const/pred_set/EMPTY' A)) | (?['f\'' : (B > A)]: (('const/pred_set/SURJ' B A) 'f\'' t s)))))).
tt('thm/pred_set/infinite_rest_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (('const/pred_set/FINITE' A) s)) => (~ (('const/pred_set/FINITE' A) (('const/pred_set/REST' A) s)))))).
tt('thm/pred_set/chooser_def_0', def, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/chooser' A) s 'const/num/0') = (('const/pred_set/CHOICE' A) s)))).
tt('thm/pred_set/chooser_def_e1', def, ![A : $t]: (![s : (A > $o), n : 'type/num/num']: ((('const/pred_set/chooser' A) s ('const/num/SUC' n)) = (('const/pred_set/chooser' A) (('const/pred_set/REST' A) s) n)))).
tt('thm/pred_set/chooser_def_compute_0', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/chooser' A) s 'const/num/0') = (('const/pred_set/CHOICE' A) s)))).
tt('thm/pred_set/chooser_def_compute_1', ax, ![A : $t]: (![s : (A > $o), n : 'type/num/num']: ((('const/pred_set/chooser' A) s ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = (('const/pred_set/chooser' A) (('const/pred_set/REST' A) s) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/pred_set/chooser_def_compute_e2', ax, ![A : $t]: (![s : (A > $o), n : 'type/num/num']: ((('const/pred_set/chooser' A) s ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = (('const/pred_set/chooser' A) (('const/pred_set/REST' A) s) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))).
tt('thm/pred_set/infinite_num_inj_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (('const/pred_set/FINITE' A) s)) = (?[f : ('type/num/num' > A)]: (('const/pred_set/INJ' 'type/num/num' A) f ('const/pred_set/UNIV' 'type/num/num') s))))).
tt('thm/pred_set/countable_def_', def, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/countable' A) s) = (?[f : (A > 'type/num/num')]: (('const/pred_set/INJ' A 'type/num/num') f s ('const/pred_set/UNIV' 'type/num/num')))))).
tt('thm/pred_set/countable_image_nats_', ax, ![A : $t]: (![f : ('type/num/num' > A)]: (('const/pred_set/countable' A) (('const/pred_set/IMAGE' 'type/num/num' A) f ('const/pred_set/UNIV' 'type/num/num'))))).
tt('thm/pred_set/countable_surj_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/countable' A) s) = ((s = ('const/pred_set/EMPTY' A)) | (?[f : ('type/num/num' > A)]: (('const/pred_set/SURJ' 'type/num/num' A) f ('const/pred_set/UNIV' 'type/num/num') s)))))).
tt('thm/pred_set/num_countable_', ax, (('const/pred_set/countable' 'type/num/num') ('const/pred_set/UNIV' 'type/num/num'))).
tt('thm/pred_set/subset_countable_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/countable' A) s) & (('const/pred_set/SUBSET' A) t s)) => (('const/pred_set/countable' A) t)))).
tt('thm/pred_set/image_countable_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: ((('const/pred_set/countable' A) s) => (('const/pred_set/countable' B) (('const/pred_set/IMAGE' A B) f s))))).
tt('thm/pred_set/finite_countable_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (('const/pred_set/countable' A) s)))).
tt('thm/pred_set/num_to_pair_def_', def, (![n : 'type/num/num']: (('const/pred_set/num_to_pair' n) = (('const/pair/,' 'type/num/num' 'type/num/num') ('const/numpair/nfst' n) ('const/numpair/nsnd' n))))).
tt('thm/pred_set/pair_to_num_def_', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/pred_set/pair_to_num' (('const/pair/,' 'type/num/num' 'type/num/num') m n)) = ('const/numpair/npair' m n)))).
tt('thm/pred_set/pair_to_num_formula_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/pred_set/pair_to_num' (('const/pair/,' 'type/num/num' 'type/num/num') x y)) = ('const/arithmetic/+' ('const/arithmetic/DIV' ('const/arithmetic/*' ('const/arithmetic/+' ('const/arithmetic/+' x y) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/+' x y)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) y)))).
tt('thm/pred_set/pair_to_num_inv_0', ax, (![x : 'type/num/num']: (('const/pred_set/pair_to_num' ('const/pred_set/num_to_pair' x)) = x))).
tt('thm/pred_set/pair_to_num_inv_e1', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/pred_set/num_to_pair' ('const/pred_set/pair_to_num' (('const/pair/,' 'type/num/num' 'type/num/num') x y))) = (('const/pair/,' 'type/num/num' 'type/num/num') x y)))).
tt('thm/pred_set/cross_countable_', ax, ![B : $t, A : $t]: (![s : (A > $o), t : (B > $o)]: (((('const/pred_set/countable' A) s) & (('const/pred_set/countable' B) t)) => (('const/pred_set/countable' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) s t))))).
tt('thm/pred_set/inter_countable_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/countable' A) s) | (('const/pred_set/countable' A) t)) => (('const/pred_set/countable' A) (('const/pred_set/INTER' A) s t))))).
tt('thm/pred_set/inj_countable_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o), t : (B > $o)]: (((('const/pred_set/countable' B) t) & (('const/pred_set/INJ' A B) f s t)) => (('const/pred_set/countable' A) s)))).
tt('thm/pred_set/bigunion_countable_', ax, ![A : $t]: (![s : ((A > $o) > $o)]: (((('const/pred_set/countable' (A > $o)) s) & (![x : (A > $o)]: ((('const/bool/IN' (A > $o)) x s) => (('const/pred_set/countable' A) x)))) => (('const/pred_set/countable' A) (('const/pred_set/BIGUNION' A) s))))).
tt('thm/pred_set/union_countable_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/countable' A) s) & (('const/pred_set/countable' A) t)) => (('const/pred_set/countable' A) (('const/pred_set/UNION' A) s t))))).
tt('thm/pred_set/union_countable_IFF_', ax, ![A : $t]: (![t : (A > $o), s : (A > $o)]: ((('const/pred_set/countable' A) (('const/pred_set/UNION' A) s t)) = ((('const/pred_set/countable' A) s) & (('const/pred_set/countable' A) t))))).
tt('thm/pred_set/inj_image_countable_IFF_', ax, ![A : $t, B : $t]: (![s : (A > $o), f : (A > B)]: ((('const/pred_set/INJ' A B) f s (('const/pred_set/IMAGE' A B) f s)) => ((('const/pred_set/countable' B) (('const/pred_set/IMAGE' A B) f s)) = (('const/pred_set/countable' A) s))))).
tt('thm/pred_set/pow_no_surj_', ax, ![A : $t]: (![s : (A > $o)]: (~ (?[f : (A > (A > $o))]: (('const/pred_set/SURJ' A (A > $o)) f s (('const/pred_set/POW' A) s)))))).
tt('thm/pred_set/infinite_pow_uncountable_', ax, ![A : $t]: (![s : (A > $o)]: ((~ (('const/pred_set/FINITE' A) s)) => (~ (('const/pred_set/countable' (A > $o)) (('const/pred_set/POW' A) s)))))).
tt('thm/pred_set/countable_Usum_', ax, ![B : $t, A : $t]: ((('const/pred_set/countable' ('type/sum/sum' A B)) ('const/pred_set/UNIV' ('type/sum/sum' A B))) = ((('const/pred_set/countable' A) ('const/pred_set/UNIV' A)) & (('const/pred_set/countable' B) ('const/pred_set/UNIV' B))))).
tt('thm/pred_set/countable_EMPTY_', ax, ![A : $t]: (('const/pred_set/countable' A) ('const/pred_set/EMPTY' A))).
tt('thm/pred_set/countable_INSERT_', ax, ![A : $t]: (![x : A, s : (A > $o)]: ((('const/pred_set/countable' A) (('const/pred_set/INSERT' A) x s)) = (('const/pred_set/countable' A) s)))).
tt('thm/pred_set/cross_countable_IFF_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o)]: ((('const/pred_set/countable' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) s t)) = ((s = ('const/pred_set/EMPTY' A)) | ((t = ('const/pred_set/EMPTY' B)) | ((('const/pred_set/countable' A) s) & (('const/pred_set/countable' B) t))))))).
tt('thm/pred_set/countable_Uprod_', ax, ![B : $t, A : $t]: ((('const/pred_set/countable' ('type/pair/prod' A B)) ('const/pred_set/UNIV' ('type/pair/prod' A B))) = ((('const/pred_set/countable' A) ('const/pred_set/UNIV' A)) & (('const/pred_set/countable' B) ('const/pred_set/UNIV' B))))).
tt('thm/pred_set/IMAGE_BIGUNION_', ax, ![A : $t, B : $t]: (![f : (A > B), M : ((A > $o) > $o)]: ((('const/pred_set/IMAGE' A B) f (('const/pred_set/BIGUNION' A) M)) = (('const/pred_set/BIGUNION' B) (('const/pred_set/IMAGE' (A > $o) (B > $o)) (('const/pred_set/IMAGE' A B) f) M))))).
tt('thm/pred_set/SUBSET_DIFF_', ax, ![A : $t]: (![s1 : (A > $o), s2 : (A > $o), s3 : (A > $o)]: ((('const/pred_set/SUBSET' A) s1 (('const/pred_set/DIFF' A) s2 s3)) = ((('const/pred_set/SUBSET' A) s1 s2) & (('const/pred_set/DISJOINT' A) s1 s3))))).
tt('thm/pred_set/INTER_SUBSET_EQN_0', ax, ![A : $t]: (![B : (A > $o), A0 : (A > $o)]: (((('const/pred_set/INTER' A) A0 B) = A0) = (('const/pred_set/SUBSET' A) A0 B)))).
tt('thm/pred_set/INTER_SUBSET_EQN_e1', ax, ![A : $t]: (![B : (A > $o), A0 : (A > $o)]: (((('const/pred_set/INTER' A) A0 B) = B) = (('const/pred_set/SUBSET' A) B A0)))).
tt('thm/pred_set/PSUBSET_SING_', ax, ![A : $t]: (![s : A, x : (A > $o)]: ((('const/pred_set/PSUBSET' A) x (('const/pred_set/INSERT' A) s ('const/pred_set/EMPTY' A))) = (x = ('const/pred_set/EMPTY' A))))).
tt('thm/pred_set/INTER_UNION_0', ax, ![A : $t]: (![B : (A > $o), A0 : (A > $o)]: ((('const/pred_set/INTER' A) (('const/pred_set/UNION' A) A0 B) A0) = A0))).
tt('thm/pred_set/INTER_UNION_1', ax, ![A : $t]: (![B : (A > $o), A0 : (A > $o)]: ((('const/pred_set/INTER' A) (('const/pred_set/UNION' A) B A0) A0) = A0))).
tt('thm/pred_set/INTER_UNION_2', ax, ![A : $t]: (![B : (A > $o), A0 : (A > $o)]: ((('const/pred_set/INTER' A) A0 (('const/pred_set/UNION' A) A0 B)) = A0))).
tt('thm/pred_set/INTER_UNION_e3', ax, ![A : $t]: (![B : (A > $o), A0 : (A > $o)]: ((('const/pred_set/INTER' A) A0 (('const/pred_set/UNION' A) B A0)) = A0))).
tt('thm/pred_set/UNION_DELETE_', ax, ![A : $t]: (![A0 : (A > $o), B : (A > $o), x : A]: ((('const/pred_set/DELETE' A) (('const/pred_set/UNION' A) A0 B) x) = (('const/pred_set/UNION' A) (('const/pred_set/DELETE' A) A0 x) (('const/pred_set/DELETE' A) B x))))).
tt('thm/pred_set/DELETE_SUBSET_INSERT_', ax, ![A : $t]: (![s : (A > $o), e : A, s2 : (A > $o)]: ((('const/pred_set/SUBSET' A) (('const/pred_set/DELETE' A) s e) s2) = (('const/pred_set/SUBSET' A) s (('const/pred_set/INSERT' A) e s2))))).
tt('thm/pred_set/IN_INSERT_EXPAND_', ax, ![A : $t]: (![x : A, y : A, P : (A > $o)]: ((('const/bool/IN' A) x (('const/pred_set/INSERT' A) y P)) = ((x = y) | ((~ (x = y)) & (('const/bool/IN' A) x P)))))).
tt('thm/pred_set/FINITE_INTER_', ax, ![A : $t]: (![s1 : (A > $o), s2 : (A > $o)]: (((('const/pred_set/FINITE' A) s1) | (('const/pred_set/FINITE' A) s2)) => (('const/pred_set/FINITE' A) (('const/pred_set/INTER' A) s1 s2))))).
tt('thm/pred_set/INSERT_EQ_SING_', ax, ![A : $t]: (![s : (A > $o), x : A, y : A]: (((('const/pred_set/INSERT' A) x s) = (('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A))) = ((x = y) & (('const/pred_set/SUBSET' A) s (('const/pred_set/INSERT' A) y ('const/pred_set/EMPTY' A))))))).
tt('thm/pred_set/CARD_UNION_LE_', ax, ![A : $t]: (![t : (A > $o), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (('const/pred_set/FINITE' A) t)) => ('const/arithmetic/<=' (('const/pred_set/CARD' A) (('const/pred_set/UNION' A) s t)) ('const/arithmetic/+' (('const/pred_set/CARD' A) s) (('const/pred_set/CARD' A) t)))))).
tt('thm/pred_set/IMAGE_SUBSET_gen_', ax, ![B : $t, A : $t]: (![f : (A > B), s : (A > $o), u : (A > $o), t : (B > $o)]: (((('const/pred_set/SUBSET' A) s u) & (('const/pred_set/SUBSET' B) (('const/pred_set/IMAGE' A B) f u) t)) => (('const/pred_set/SUBSET' B) (('const/pred_set/IMAGE' A B) f s) t)))).
tt('thm/pred_set/CARD_REST_', ax, ![A : $t]: (![s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (~ (s = ('const/pred_set/EMPTY' A)))) => ((('const/pred_set/CARD' A) (('const/pred_set/REST' A) s)) = ('const/arithmetic/-' (('const/pred_set/CARD' A) s) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/pred_set/SUBSET_DIFF_EMPTY_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: (((('const/pred_set/DIFF' A) s t) = ('const/pred_set/EMPTY' A)) = (('const/pred_set/SUBSET' A) s t)))).
tt('thm/pred_set/DIFF_INTER_SUBSET_', ax, ![A : $t]: (![r : (A > $o), s : (A > $o), t : (A > $o)]: ((('const/pred_set/SUBSET' A) r s) => ((('const/pred_set/DIFF' A) r (('const/pred_set/INTER' A) s t)) = (('const/pred_set/DIFF' A) r t))))).
tt('thm/pred_set/UNION_DIFF_2_', ax, ![A : $t]: (![s : (A > $o), t : (A > $o)]: ((('const/pred_set/UNION' A) s (('const/pred_set/DIFF' A) s t)) = s))).
tt('thm/pred_set/count_add_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/pred_set/count' ('const/arithmetic/+' n m)) = (('const/pred_set/UNION' 'type/num/num') ('const/pred_set/count' n) (('const/pred_set/IMAGE' 'type/num/num' 'type/num/num') ('const/arithmetic/+' n) ('const/pred_set/count' m)))))).
tt('thm/pred_set/IMAGE_EQ_SING_', ax, ![A : $t, B : $t]: (![z : A, s : (B > $o), f : (B > A)]: (((('const/pred_set/IMAGE' B A) f s) = (('const/pred_set/INSERT' A) z ('const/pred_set/EMPTY' A))) = ((~ (s = ('const/pred_set/EMPTY' B))) & (![x : B]: ((('const/bool/IN' B) x s) => ((f x) = z))))))).
tt('thm/pred_set/count_add1_', ax, (![n : 'type/num/num']: (('const/pred_set/count' ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (('const/pred_set/INSERT' 'type/num/num') n ('const/pred_set/count' n))))).
tt('thm/pred_set/compl_insert_', ax, ![A : $t]: (![s : (A > $o), x : A]: ((('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x s)) = (('const/pred_set/DELETE' A) (('const/pred_set/COMPL' A) s) x)))).
tt('thm/pred_set/in_max_set_', ax, (![s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (![x : 'type/num/num']: ((('const/bool/IN' 'type/num/num') x s) => ('const/arithmetic/<=' x ('const/pred_set/MAX_SET' s))))))).
