tt('const/set_relation/RREFL_EXP', ty, ![A : $t]: ((A > (A > $o)) > ((A > $o) > (A > (A > $o))))).
tt('const/set_relation/RRUNIV', ty, ![A : $t]: ((A > $o) > (A > (A > $o)))).
tt('const/set_relation/acyclic', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > $o)).
tt('const/set_relation/all_choices', ty, ![A : $t]: (((A > $o) > $o) > ((A > $o) > $o))).
tt('const/set_relation/antisym', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > $o)).
tt('const/set_relation/chain', ty, ![A : $t]: ((A > $o) > ((('type/pair/prod' A A) > $o) > $o))).
tt('const/set_relation/domain', ty, ![A : $t, B : $t]: ((('type/pair/prod' A B) > $o) > (A > $o))).
tt('const/set_relation/fchains', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > $o))).
tt('const/set_relation/finite_prefixes', ty, ![A : $t, B : $t]: ((('type/pair/prod' A B) > $o) > ((B > $o) > $o))).
tt('const/set_relation/get_min', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > (('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) > ('type/option/option' A)))).
tt('const/set_relation/irreflexive', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > $o))).
tt('const/set_relation/linear_order', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > $o))).
tt('const/set_relation/maximal_elements', ty, ![A : $t]: ((A > $o) > ((('type/pair/prod' A A) > $o) > (A > $o)))).
tt('const/set_relation/minimal_elements', ty, ![A : $t]: ((A > $o) > ((('type/pair/prod' A A) > $o) > (A > $o)))).
tt('const/set_relation/nth_min', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > (('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) > ('type/num/num' > ('type/option/option' A))))).
tt('const/set_relation/nth_min_tupled', ty, ![A : $t]: (('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) > ('type/option/option' A))).
tt('const/set_relation/num_order', ty, ![A : $t]: ((A > 'type/num/num') > ((A > $o) > (('type/pair/prod' A A) > $o)))).
tt('const/set_relation/partial_order', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > $o))).
tt('const/set_relation/per', ty, ![A : $t]: ((A > $o) > (((A > $o) > $o) > $o))).
tt('const/set_relation/per_restrict', ty, ![A : $t]: (((A > $o) > $o) > ((A > $o) > ((A > $o) > $o)))).
tt('const/set_relation/range', ty, ![A : $t, B : $t]: ((('type/pair/prod' B A) > $o) > (A > $o))).
tt('const/set_relation/rcomp', ty, ![A : $t, B : $t, C : $t]: ((('type/pair/prod' A C) > $o) > ((('type/pair/prod' C B) > $o) > (('type/pair/prod' A B) > $o)))).
tt('const/set_relation/reflexive', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > $o))).
tt('const/set_relation/rel_to_reln', ty, ![A : $t, B : $t]: ((A > (B > $o)) > (('type/pair/prod' A B) > $o))).
tt('const/set_relation/reln_to_rel', ty, ![A : $t, B : $t]: ((('type/pair/prod' A B) > $o) > (A > (B > $o)))).
tt('const/set_relation/rrestrict', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > (('type/pair/prod' A A) > $o)))).
tt('const/set_relation/strict', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > (('type/pair/prod' A A) > $o))).
tt('const/set_relation/strict_linear_order', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > ((A > $o) > $o))).
tt('const/set_relation/tc', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > (('type/pair/prod' A A) > $o))).
tt('const/set_relation/transitive', ty, ![A : $t]: ((('type/pair/prod' A A) > $o) > $o)).
tt('const/set_relation/univ_reln', ty, ![A : $t]: ((A > $o) > (('type/pair/prod' A A) > $o))).
tt('const/set_relation/upper_bounds', ty, ![A : $t, B : $t]: ((B > $o) > ((('type/pair/prod' B A) > $o) > (A > $o)))).
tt('thm/set_relation/rextension_', ax, ![A : $t, B : $t]: (![s : (('type/pair/prod' A B) > $o), t : (('type/pair/prod' A B) > $o)]: ((s = t) = (![x : A, y : B]: ((('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) s) = (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) t)))))).
tt('thm/set_relation/domain_def_', def, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/domain' A B) r) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (?[y : B]: (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) r)))))))).
tt('thm/set_relation/range_def_', def, ![B : $t, A : $t]: (![r : (('type/pair/prod' B A) > $o)]: ((('const/set_relation/range' A B) r) = (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (?[x : B]: (('const/bool/IN' ('type/pair/prod' B A)) (('const/pair/,' B A) x y) r)))))))).
tt('thm/set_relation/in_domain_', ax, ![A : $t, B : $t]: (![x : A, r : (('type/pair/prod' A B) > $o)]: ((('const/bool/IN' A) x (('const/set_relation/domain' A B) r)) = (?[y : B]: (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) r))))).
tt('thm/set_relation/in_range_', ax, ![B : $t, A : $t]: (![y : A, r : (('type/pair/prod' B A) > $o)]: ((('const/bool/IN' A) y (('const/set_relation/range' A B) r)) = (?[x : B]: (('const/bool/IN' ('type/pair/prod' B A)) (('const/pair/,' B A) x y) r))))).
tt('thm/set_relation/rrestrict_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/rrestrict' A) r s) = (('const/pred_set/GSPEC' ('type/pair/prod' A A) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' A A) $o)) (^[x : A, y : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x y) ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & ((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)))))))))).
tt('thm/set_relation/in_rrestrict_', ax, ![A : $t]: (![x : A, y : A, r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/rrestrict' A) r s)) = ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & ((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)))))).
tt('thm/set_relation/rrestrict_union_', ax, ![A : $t]: (![r1 : (('type/pair/prod' A A) > $o), r2 : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/rrestrict' A) (('const/pred_set/UNION' ('type/pair/prod' A A)) r1 r2) s) = (('const/pred_set/UNION' ('type/pair/prod' A A)) (('const/set_relation/rrestrict' A) r1 s) (('const/set_relation/rrestrict' A) r2 s))))).
tt('thm/set_relation/rrestrict_rrestrict_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : (A > $o), y : (A > $o)]: ((('const/set_relation/rrestrict' A) (('const/set_relation/rrestrict' A) r x) y) = (('const/set_relation/rrestrict' A) r (('const/pred_set/INTER' A) x y))))).
tt('thm/set_relation/rcomp_def_', def, ![C : $t, B : $t, A : $t]: (![r1 : (('type/pair/prod' A C) > $o), r2 : (('type/pair/prod' C B) > $o)]: ((('const/set_relation/rcomp' A B C) r1 r2) = (('const/pred_set/GSPEC' ('type/pair/prod' A B) ('type/pair/prod' A B)) (('const/pair/UNCURRY' A B ('type/pair/prod' ('type/pair/prod' A B) $o)) (^[x : A, y : B]: (('const/pair/,' ('type/pair/prod' A B) $o) (('const/pair/,' A B) x y) (?[z : C]: ((('const/bool/IN' ('type/pair/prod' A C)) (('const/pair/,' A C) x z) r1) & (('const/bool/IN' ('type/pair/prod' C B)) (('const/pair/,' C B) z y) r2)))))))))).
tt('thm/set_relation/strict_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/strict' A) r) = (('const/pred_set/GSPEC' ('type/pair/prod' A A) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' A A) $o)) (^[x : A, y : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x y) ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & (~ (x = y)))))))))).
tt('thm/set_relation/strict_rrestrict_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/strict' A) (('const/set_relation/rrestrict' A) r s)) = (('const/set_relation/rrestrict' A) (('const/set_relation/strict' A) r) s)))).
tt('thm/set_relation/univ_reln_def_', def, ![A : $t]: (![xs : (A > $o)]: ((('const/set_relation/univ_reln' A) xs) = (('const/pred_set/GSPEC' ('type/pair/prod' A A) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' A A) $o)) (^[x1 : A, x2 : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x1 x2) ((('const/bool/IN' A) x1 xs) & (('const/bool/IN' A) x2 xs))))))))).
tt('thm/set_relation/finite_prefixes_def_', def, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o), s : (B > $o)]: ((('const/set_relation/finite_prefixes' A B) r s) = (![e : B]: ((('const/bool/IN' B) e s) => (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^['e\'' : A]: (('const/pair/,' A $o) 'e\'' (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) 'e\'' e) r)))))))))).
tt('thm/set_relation/finite_prefixes_subset_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), 's\'' : (A > $o)]: (((('const/set_relation/finite_prefixes' A A) r s) & (('const/pred_set/SUBSET' A) 's\'' s)) => ((('const/set_relation/finite_prefixes' A A) r 's\'') & (('const/set_relation/finite_prefixes' A A) (('const/set_relation/rrestrict' A) r 's\'') 's\''))))).
tt('thm/set_relation/finite_prefixes_union_', ax, ![B : $t, A : $t]: (![r1 : (('type/pair/prod' A B) > $o), r2 : (('type/pair/prod' A B) > $o), s1 : (B > $o), s2 : (B > $o)]: (((('const/set_relation/finite_prefixes' A B) r1 s1) & (('const/set_relation/finite_prefixes' A B) r2 s2)) => (('const/set_relation/finite_prefixes' A B) (('const/pred_set/UNION' ('type/pair/prod' A B)) r1 r2) (('const/pred_set/INTER' B) s1 s2))))).
tt('thm/set_relation/finite_prefixes_comp_', ax, ![C : $t, B : $t, A : $t]: (![r1 : (('type/pair/prod' A B) > $o), r2 : (('type/pair/prod' B C) > $o), s1 : (B > $o), s2 : (C > $o)]: (((('const/set_relation/finite_prefixes' A B) r1 s1) & ((('const/set_relation/finite_prefixes' B C) r2 s2) & (('const/pred_set/SUBSET' B) (('const/pred_set/GSPEC' B B) (^[x : B]: (('const/pair/,' B $o) x (?[y : C]: ((('const/bool/IN' C) y s2) & (('const/bool/IN' ('type/pair/prod' B C)) (('const/pair/,' B C) x y) r2)))))) s1))) => (('const/set_relation/finite_prefixes' A C) (('const/set_relation/rcomp' A C B) r1 r2) s2)))).
tt('thm/set_relation/finite_prefixes_inj_image_', ax, ![A : $t, B : $t]: (![f : (A > B), r : (('type/pair/prod' A A) > $o), s : (A > $o)]: (((![x : A, y : A]: (((f x) = (f y)) => (x = y))) & (('const/set_relation/finite_prefixes' A A) r s)) => (('const/set_relation/finite_prefixes' B B) (('const/pred_set/GSPEC' ('type/pair/prod' B B) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' B B) $o)) (^[x : A, y : A]: (('const/pair/,' ('type/pair/prod' B B) $o) (('const/pair/,' B B) (f x) (f y)) (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r))))) (('const/pred_set/IMAGE' A B) f s))))).
tt('thm/set_relation/finite_prefixes_range_', ax, ![B : $t, A : $t]: (![r : (('type/pair/prod' A B) > $o), s : (B > $o), t : (B > $o)]: (((('const/set_relation/finite_prefixes' A B) r s) & (('const/pred_set/DISJOINT' B) t (('const/set_relation/range' B A) r))) => (('const/set_relation/finite_prefixes' A B) r (('const/pred_set/UNION' B) s t))))).
tt('thm/set_relation/tc_def_', def, ![A : $t]: (('const/set_relation/tc' A) = (^[r : (('type/pair/prod' A A) > $o), a0 : ('type/pair/prod' A A)]: (!['tc\'' : (('type/pair/prod' A A) > $o)]: ((![a00 : ('type/pair/prod' A A)]: (((?[x : A, y : A]: ((a00 = (('const/pair/,' A A) x y)) & (r (('const/pair/,' A A) x y)))) | (?[x : A, y : A]: ((a00 = (('const/pair/,' A A) x y)) & (?[z : A]: (('tc\'' (('const/pair/,' A A) x z)) & ('tc\'' (('const/pair/,' A A) z y))))))) => ('tc\'' a00))) => ('tc\'' a0)))))).
tt('thm/set_relation/tc_rules_0', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r))))).
tt('thm/set_relation/tc_rules_e1', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A, y : A]: ((?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) (('const/set_relation/tc' A) r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) (('const/set_relation/tc' A) r)))) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r))))).
tt('thm/set_relation/tc_cases_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) = ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) | (?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) (('const/set_relation/tc' A) r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) (('const/set_relation/tc' A) r)))))))).
tt('thm/set_relation/tc_ind_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => ('tc\'' x y))) & (![x : A, y : A]: ((?[z : A]: (('tc\'' x z) & ('tc\'' z y))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/tc_strongind_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => ('tc\'' x y))) & (![x : A, y : A]: ((?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) (('const/set_relation/tc' A) r)) & (('tc\'' x z) & ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) (('const/set_relation/tc' A) r)) & ('tc\'' z y))))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/tc_cases_right_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) = ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) | (?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) (('const/set_relation/tc' A) r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) r))))))).
tt('thm/set_relation/tc_cases_left_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) = ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) | (?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) r) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) (('const/set_relation/tc' A) r)))))))).
tt('thm/set_relation/tc_ind_left_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => ('tc\'' x y))) & (![x : A, y : A]: ((?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) r) & ('tc\'' z y))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/tc_strongind_left_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => ('tc\'' x y))) & (![x : A, y : A]: ((?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) r) & ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) (('const/set_relation/tc' A) r)) & ('tc\'' z y)))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/tc_ind_right_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => ('tc\'' x y))) & (![x : A, y : A]: ((?[z : A]: (('tc\'' x z) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) r))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/rtc_ind_right_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A]: (((('const/bool/IN' A) x (('const/set_relation/domain' A A) r)) | (('const/bool/IN' A) x (('const/set_relation/range' A A) r))) => ('tc\'' x x))) & (![x : A, y : A]: ((?[z : A]: (('tc\'' x z) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) r))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/tc_strongind_right_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'tc\'' : (A > (A > $o))]: (((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) => ('tc\'' x y))) & (![x : A, y : A]: ((?[z : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) (('const/set_relation/tc' A) r)) & (('tc\'' x z) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) z y) r)))) => ('tc\'' x y)))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ('tc\'' x y)))))).
tt('thm/set_relation/tc_union_', ax, ![A : $t]: (![r1 : (('type/pair/prod' A A) > $o), x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r1)) => (![r2 : (('type/pair/prod' A A) > $o)]: (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) (('const/pred_set/UNION' ('type/pair/prod' A A)) r1 r2))))))).
tt('thm/set_relation/tc_implication_', ax, ![A : $t]: (![r1 : (('type/pair/prod' A A) > $o), r2 : (('type/pair/prod' A A) > $o)]: ((![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r1) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r2))) => (![x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r1)) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r2))))))).
tt('thm/set_relation/tc_empty_', ax, ![A : $t]: (![x : A, y : A]: (~ (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) ('const/pred_set/EMPTY' ('type/pair/prod' A A))))))).
tt('thm/set_relation/tc_domain_range_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A, y : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r)) => ((('const/bool/IN' A) x (('const/set_relation/domain' A A) r)) & (('const/bool/IN' A) y (('const/set_relation/range' A A) r)))))).
tt('thm/set_relation/rrestrict_tc_', ax, ![A : $t]: (![x : (A > $o), r : (('type/pair/prod' A A) > $o), e : A, 'e\'' : A]: ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) e 'e\'') (('const/set_relation/tc' A) (('const/set_relation/rrestrict' A) r x))) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) e 'e\'') (('const/set_relation/tc' A) r))))).
tt('thm/set_relation/acyclic_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/acyclic' A) r) = (![x : A]: (~ (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x x) (('const/set_relation/tc' A) r))))))).
tt('thm/set_relation/acyclic_subset_', ax, ![A : $t]: (![r1 : (('type/pair/prod' A A) > $o), r2 : (('type/pair/prod' A A) > $o)]: (((('const/set_relation/acyclic' A) r1) & (('const/pred_set/SUBSET' ('type/pair/prod' A A)) r2 r1)) => (('const/set_relation/acyclic' A) r2)))).
tt('thm/set_relation/acyclic_rrestrict_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/acyclic' A) r) => (('const/set_relation/acyclic' A) (('const/set_relation/rrestrict' A) r s))))).
tt('thm/set_relation/acyclic_irreflexive_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), x : A]: ((('const/set_relation/acyclic' A) r) => (~ (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x x) r))))).
tt('thm/set_relation/acyclic_bigunion_', ax, ![A : $t]: (![rs : ((('type/pair/prod' A A) > $o) > $o)]: (((![r : (('type/pair/prod' A A) > $o), 'r\'' : (('type/pair/prod' A A) > $o)]: (((('const/bool/IN' (('type/pair/prod' A A) > $o)) r rs) & ((('const/bool/IN' (('type/pair/prod' A A) > $o)) 'r\'' rs) & (~ (r = 'r\'')))) => (('const/pred_set/DISJOINT' A) (('const/pred_set/UNION' A) (('const/set_relation/domain' A A) r) (('const/set_relation/range' A A) r)) (('const/pred_set/UNION' A) (('const/set_relation/domain' A A) 'r\'') (('const/set_relation/range' A A) 'r\''))))) & (![r : (('type/pair/prod' A A) > $o)]: ((('const/bool/IN' (('type/pair/prod' A A) > $o)) r rs) => (('const/set_relation/acyclic' A) r)))) => (('const/set_relation/acyclic' A) (('const/pred_set/BIGUNION' ('type/pair/prod' A A)) rs))))).
tt('thm/set_relation/acyclic_union_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), 'r\'' : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/DISJOINT' A) (('const/pred_set/UNION' A) (('const/set_relation/domain' A A) r) (('const/set_relation/range' A A) r)) (('const/pred_set/UNION' A) (('const/set_relation/domain' A A) 'r\'') (('const/set_relation/range' A A) 'r\''))) & ((('const/set_relation/acyclic' A) r) & (('const/set_relation/acyclic' A) 'r\''))) => (('const/set_relation/acyclic' A) (('const/pred_set/UNION' ('type/pair/prod' A A)) r 'r\''))))).
tt('thm/set_relation/maximal_elements_def_', def, ![A : $t]: (![xs : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/maximal_elements' A) xs r) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x xs) & (!['x\'' : A]: (((('const/bool/IN' A) 'x\'' xs) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x 'x\'') r)) => (x = 'x\'')))))))))).
tt('thm/set_relation/minimal_elements_def_', def, ![A : $t]: (![xs : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/minimal_elements' A) xs r) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x xs) & (!['x\'' : A]: (((('const/bool/IN' A) 'x\'' xs) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) 'x\'' x) r)) => (x = 'x\'')))))))))).
tt('thm/set_relation/maximal_union_', ax, ![A : $t]: (![e : A, s : (A > $o), r1 : (('type/pair/prod' A A) > $o), r2 : (('type/pair/prod' A A) > $o)]: ((('const/bool/IN' A) e (('const/set_relation/maximal_elements' A) s (('const/pred_set/UNION' ('type/pair/prod' A A)) r1 r2))) => ((('const/bool/IN' A) e (('const/set_relation/maximal_elements' A) s r1)) & (('const/bool/IN' A) e (('const/set_relation/maximal_elements' A) s r2)))))).
tt('thm/set_relation/minimal_union_', ax, ![A : $t]: (![e : A, s : (A > $o), r1 : (('type/pair/prod' A A) > $o), r2 : (('type/pair/prod' A A) > $o)]: ((('const/bool/IN' A) e (('const/set_relation/minimal_elements' A) s (('const/pred_set/UNION' ('type/pair/prod' A A)) r1 r2))) => ((('const/bool/IN' A) e (('const/set_relation/minimal_elements' A) s r1)) & (('const/bool/IN' A) e (('const/set_relation/minimal_elements' A) s r2)))))).
tt('thm/set_relation/finite_acyclic_has_maximal_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((~ (s = ('const/pred_set/EMPTY' A))) => (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/acyclic' A) r) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/maximal_elements' A) s r))))))))).
tt('thm/set_relation/finite_acyclic_has_minimal_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((~ (s = ('const/pred_set/EMPTY' A))) => (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/acyclic' A) r) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) s r))))))))).
tt('thm/set_relation/maximal_TC_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) r) s) & (('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) r) s)) => ((('const/set_relation/maximal_elements' A) s (('const/set_relation/tc' A) r)) = (('const/set_relation/maximal_elements' A) s r))))).
tt('thm/set_relation/minimal_TC_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) r) s) & (('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) r) s)) => ((('const/set_relation/minimal_elements' A) s (('const/set_relation/tc' A) r)) = (('const/set_relation/minimal_elements' A) s r))))).
tt('thm/set_relation/finite_acyclic_has_maximal_path_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o), x : A]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/acyclic' A) r) & ((('const/bool/IN' A) x s) & (~ (('const/bool/IN' A) x (('const/set_relation/maximal_elements' A) s r)))))) => (?[y : A]: ((('const/bool/IN' A) y (('const/set_relation/maximal_elements' A) s r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) (('const/set_relation/tc' A) r))))))).
tt('thm/set_relation/finite_acyclic_has_minimal_path_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o), x : A]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/acyclic' A) r) & ((('const/bool/IN' A) x s) & (~ (('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) s r)))))) => (?[y : A]: ((('const/bool/IN' A) y (('const/set_relation/minimal_elements' A) s r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y x) (('const/set_relation/tc' A) r))))))).
tt('thm/set_relation/reflexive_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/reflexive' A) r s) = (![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x x) r)))))).
tt('thm/set_relation/irreflexive_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/irreflexive' A) r s) = (![x : A]: ((('const/bool/IN' A) x s) => (~ (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x x) r))))))).
tt('thm/set_relation/transitive_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/transitive' A) r) = (![x : A, y : A, z : A]: (((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y z) r)) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x z) r)))))).
tt('thm/set_relation/transitive_tc_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/transitive' A) r) => ((('const/set_relation/tc' A) r) = r)))).
tt('thm/set_relation/tc_transitive_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: (('const/set_relation/transitive' A) (('const/set_relation/tc' A) r)))).
tt('thm/set_relation/antisym_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/antisym' A) r) = (![x : A, y : A]: (((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y x) r)) => (x = y)))))).
tt('thm/set_relation/partial_order_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/partial_order' A) r s) = ((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) r) s) & ((('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) r) s) & ((('const/set_relation/transitive' A) r) & ((('const/set_relation/reflexive' A) r s) & (('const/set_relation/antisym' A) r)))))))).
tt('thm/set_relation/partial_order_dom_rng_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), x : A, y : A]: (((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & (('const/set_relation/partial_order' A) r s)) => ((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s))))).
tt('thm/set_relation/partial_order_subset_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), 's\'' : (A > $o)]: (((('const/set_relation/partial_order' A) r s) & (('const/pred_set/SUBSET' A) 's\'' s)) => (('const/set_relation/partial_order' A) (('const/set_relation/rrestrict' A) r 's\'') 's\'')))).
tt('thm/set_relation/strict_partial_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/partial_order' A) r s) => ((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) (('const/set_relation/strict' A) r)) s) & ((('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) (('const/set_relation/strict' A) r)) s) & ((('const/set_relation/transitive' A) (('const/set_relation/strict' A) r)) & (('const/set_relation/antisym' A) (('const/set_relation/strict' A) r)))))))).
tt('thm/set_relation/strict_partial_order_acyclic_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/partial_order' A) r s) => (('const/set_relation/acyclic' A) (('const/set_relation/strict' A) r))))).
tt('thm/set_relation/finite_prefix_po_has_minimal_path_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), x : A, 's\'' : (A > $o)]: (((('const/set_relation/partial_order' A) r s) & ((('const/set_relation/finite_prefixes' A A) r s) & ((~ (('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) 's\'' r))) & ((('const/bool/IN' A) x 's\'') & (('const/pred_set/SUBSET' A) 's\'' s))))) => (?['x\'' : A]: ((('const/bool/IN' A) 'x\'' (('const/set_relation/minimal_elements' A) 's\'' r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) 'x\'' x) r)))))).
tt('thm/set_relation/linear_order_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/linear_order' A) r s) = ((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) r) s) & ((('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) r) s) & ((('const/set_relation/transitive' A) r) & ((('const/set_relation/antisym' A) r) & (![x : A, y : A]: (((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)) => ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) | (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y x) r))))))))))).
tt('thm/set_relation/linear_order_subset_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), 's\'' : (A > $o)]: (((('const/set_relation/linear_order' A) r s) & (('const/pred_set/SUBSET' A) 's\'' s)) => (('const/set_relation/linear_order' A) (('const/set_relation/rrestrict' A) r 's\'') 's\'')))).
tt('thm/set_relation/partial_order_linear_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/linear_order' A) r s) => (('const/set_relation/partial_order' A) r s)))).
tt('thm/set_relation/strict_linear_order_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/strict_linear_order' A) r s) = ((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) r) s) & ((('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) r) s) & ((('const/set_relation/transitive' A) r) & ((![x : A]: (~ (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x x) r))) & (![x : A, y : A]: (((('const/bool/IN' A) x s) & ((('const/bool/IN' A) y s) & (~ (x = y)))) => ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) | (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y x) r))))))))))).
tt('thm/set_relation/strict_linear_order_dom_rng_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), x : A, y : A]: (((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & (('const/set_relation/strict_linear_order' A) r s)) => ((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s))))).
tt('thm/set_relation/linear_order_dom_rng_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), x : A, y : A]: (((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) & (('const/set_relation/linear_order' A) r s)) => ((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s))))).
tt('thm/set_relation/empty_strict_linear_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/strict_linear_order' A) r ('const/pred_set/EMPTY' A)) = (r = ('const/pred_set/EMPTY' ('type/pair/prod' A A)))))).
tt('thm/set_relation/empty_linear_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/linear_order' A) r ('const/pred_set/EMPTY' A)) = (r = ('const/pred_set/EMPTY' ('type/pair/prod' A A)))))).
tt('thm/set_relation/linear_order_restrict_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o), 's\'' : (A > $o)]: ((('const/set_relation/linear_order' A) r s) => (('const/set_relation/linear_order' A) (('const/set_relation/rrestrict' A) r 's\'') (('const/pred_set/INTER' A) s 's\''))))).
tt('thm/set_relation/strict_linear_order_restrict_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o), 's\'' : (A > $o)]: ((('const/set_relation/strict_linear_order' A) r s) => (('const/set_relation/strict_linear_order' A) (('const/set_relation/rrestrict' A) r 's\'') (('const/pred_set/INTER' A) s 's\''))))).
tt('thm/set_relation/extend_linear_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), x : A]: (((~ (('const/bool/IN' A) x s)) & (('const/set_relation/linear_order' A) r s)) => (('const/set_relation/linear_order' A) (('const/pred_set/UNION' ('type/pair/prod' A A)) r (('const/pred_set/GSPEC' ('type/pair/prod' A A) A) (^[y : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) y x) (('const/bool/IN' A) y (('const/pred_set/UNION' A) s (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))))))) (('const/pred_set/UNION' A) s (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))))).
tt('thm/set_relation/strict_linear_order_acyclic_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/strict_linear_order' A) r s) => (('const/set_relation/acyclic' A) r)))).
tt('thm/set_relation/strict_linear_order_union_acyclic_', ax, ![A : $t]: (![r1 : (('type/pair/prod' A A) > $o), r2 : (('type/pair/prod' A A) > $o), s : (A > $o)]: (((('const/set_relation/strict_linear_order' A) r1 s) & (('const/pred_set/SUBSET' A) (('const/pred_set/UNION' A) (('const/set_relation/domain' A A) r2) (('const/set_relation/range' A A) r2)) s)) => ((('const/set_relation/acyclic' A) (('const/pred_set/UNION' ('type/pair/prod' A A)) r1 r2)) = (('const/pred_set/SUBSET' ('type/pair/prod' A A)) r2 r1))))).
tt('thm/set_relation/strict_linear_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/linear_order' A) r s) => (('const/set_relation/strict_linear_order' A) (('const/set_relation/strict' A) r) s)))).
tt('thm/set_relation/linear_order_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: ((('const/set_relation/strict_linear_order' A) r s) => (('const/set_relation/linear_order' A) (('const/pred_set/UNION' ('type/pair/prod' A A)) r (('const/pred_set/GSPEC' ('type/pair/prod' A A) A) (^[x : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x x) (('const/bool/IN' A) x s))))) s)))).
tt('thm/set_relation/finite_strict_linear_order_has_maximal_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/strict_linear_order' A) r s) & (~ (s = ('const/pred_set/EMPTY' A))))) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/maximal_elements' A) s r)))))).
tt('thm/set_relation/finite_strict_linear_order_has_minimal_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/strict_linear_order' A) r s) & (~ (s = ('const/pred_set/EMPTY' A))))) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) s r)))))).
tt('thm/set_relation/finite_linear_order_has_maximal_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/linear_order' A) r s) & (~ (s = ('const/pred_set/EMPTY' A))))) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/maximal_elements' A) s r)))))).
tt('thm/set_relation/finite_linear_order_has_minimal_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/linear_order' A) r s) & (~ (s = ('const/pred_set/EMPTY' A))))) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) s r)))))).
tt('thm/set_relation/maximal_linear_order_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o), x : A, y : A]: (((('const/bool/IN' A) y s) & ((('const/set_relation/linear_order' A) r s) & (('const/bool/IN' A) x (('const/set_relation/maximal_elements' A) s r)))) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y x) r)))).
tt('thm/set_relation/minimal_linear_order_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o), x : A, y : A]: (((('const/bool/IN' A) y s) & ((('const/set_relation/linear_order' A) r s) & (('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) s r)))) => (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r)))).
tt('thm/set_relation/minimal_linear_order_unique_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), 's\'' : (A > $o), x : A, y : A]: (((('const/set_relation/linear_order' A) r s) & ((('const/bool/IN' A) x (('const/set_relation/minimal_elements' A) 's\'' r)) & ((('const/bool/IN' A) y (('const/set_relation/minimal_elements' A) 's\'' r)) & (('const/pred_set/SUBSET' A) 's\'' s)))) => (x = y)))).
tt('thm/set_relation/finite_prefix_linear_order_has_unique_minimal_', ax, ![A : $t]: (![x : A, r : (('type/pair/prod' A A) > $o), s : (A > $o), 's\'' : (A > $o)]: (((('const/set_relation/linear_order' A) r s) & ((('const/set_relation/finite_prefixes' A A) r s) & ((('const/bool/IN' A) x 's\'') & (('const/pred_set/SUBSET' A) 's\'' s)))) => (('const/pred_set/SING' A) (('const/set_relation/minimal_elements' A) 's\'' r))))).
tt('thm/set_relation/nat_order_iso_thm_', ax, ![A : $t]: (![f : ('type/num/num' > ('type/option/option' A)), s : (A > $o)]: (((![n : 'type/num/num', m : 'type/num/num']: ((((f m) = (f n)) & (~ ((f m) = ('const/option/NONE' A)))) => (m = n))) & ((![x : A]: ((('const/bool/IN' A) x s) => (?[m : 'type/num/num']: ((f m) = (('const/option/SOME' A) x))))) & (![m : 'type/num/num', x : A]: (((f m) = (('const/option/SOME' A) x)) => (('const/bool/IN' A) x s))))) => ((('const/set_relation/linear_order' A) (('const/pred_set/GSPEC' ('type/pair/prod' A A) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' A A) $o)) (^[x : A, y : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x y) (?[m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) & (((f m) = (('const/option/SOME' A) x)) & ((f n) = (('const/option/SOME' A) y))))))))) s) & (('const/set_relation/finite_prefixes' A A) (('const/pred_set/GSPEC' ('type/pair/prod' A A) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' A A) $o)) (^[x : A, y : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x y) (?[m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) & (((f m) = (('const/option/SOME' A) x)) & ((f n) = (('const/option/SOME' A) y))))))))) s))))).
tt('thm/set_relation/chain_def_', def, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/chain' A) s r) = (![x : A, y : A]: (((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)) => ((('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x y) r) | (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) y x) r))))))).
tt('thm/set_relation/upper_bounds_def_', def, ![B : $t, A : $t]: (![s : (B > $o), r : (('type/pair/prod' B A) > $o)]: ((('const/set_relation/upper_bounds' A B) s r) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/set_relation/range' A B) r)) & (![y : B]: ((('const/bool/IN' B) y s) => (('const/bool/IN' ('type/pair/prod' B A)) (('const/pair/,' B A) y x) r)))))))))).
tt('thm/set_relation/upper_bounds_lem_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o), x1 : A, x2 : A]: (((('const/set_relation/transitive' A) r) & ((('const/bool/IN' A) x1 (('const/set_relation/upper_bounds' A A) s r)) & (('const/bool/IN' ('type/pair/prod' A A)) (('const/pair/,' A A) x1 x2) r))) => (('const/bool/IN' A) x2 (('const/set_relation/upper_bounds' A A) s r))))).
tt('thm/set_relation/fchains_def_', def, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/fchains' A) r) = (('const/pred_set/GSPEC' (A > $o) (A > $o)) (^[k : (A > $o)]: (('const/pair/,' (A > $o) $o) k ((('const/set_relation/chain' A) k r) & ((~ (k = ('const/pred_set/EMPTY' A))) & (![C : (A > $o)]: (((('const/set_relation/chain' A) C r) & ((('const/pred_set/SUBSET' A) C k) & (~ ((('const/pred_set/INTER' A) (('const/pred_set/DIFF' A) (('const/set_relation/upper_bounds' A A) C r) C) k) = ('const/pred_set/EMPTY' A))))) => (('const/bool/IN' A) (('const/pred_set/CHOICE' A) (('const/pred_set/DIFF' A) (('const/set_relation/upper_bounds' A A) C r) C)) (('const/set_relation/minimal_elements' A) (('const/pred_set/INTER' A) (('const/pred_set/DIFF' A) (('const/set_relation/upper_bounds' A A) C r) C) k) r)))))))))))).
tt('thm/set_relation/zorns_lemma_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: (((~ (s = ('const/pred_set/EMPTY' A))) & ((('const/set_relation/partial_order' A) r s) & (![t : (A > $o)]: ((('const/set_relation/chain' A) t r) => (~ ((('const/set_relation/upper_bounds' A A) t r) = ('const/pred_set/EMPTY' A))))))) => (?[x : A]: (('const/bool/IN' A) x (('const/set_relation/maximal_elements' A) s r)))))).
tt('thm/set_relation/per_def_', def, ![A : $t]: (![xs : (A > $o), xss : ((A > $o) > $o)]: ((('const/set_relation/per' A) xs xss) = ((('const/pred_set/SUBSET' A) (('const/pred_set/BIGUNION' A) xss) xs) & ((~ (('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) xss)) & (![xs1 : (A > $o), xs2 : (A > $o)]: (((('const/bool/IN' (A > $o)) xs1 xss) & ((('const/bool/IN' (A > $o)) xs2 xss) & (~ (xs1 = xs2)))) => (('const/pred_set/DISJOINT' A) xs1 xs2)))))))).
tt('thm/set_relation/per_restrict_def_', def, ![A : $t]: (![xss : ((A > $o) > $o), xs : (A > $o)]: ((('const/set_relation/per_restrict' A) xss xs) = (('const/pred_set/DELETE' (A > $o)) (('const/pred_set/GSPEC' (A > $o) (A > $o)) (^['xs\'' : (A > $o)]: (('const/pair/,' (A > $o) $o) (('const/pred_set/INTER' A) 'xs\'' xs) (('const/bool/IN' (A > $o)) 'xs\'' xss)))) ('const/pred_set/EMPTY' A))))).
tt('thm/set_relation/per_delete_', ax, ![A : $t]: (![xs : (A > $o), xss : ((A > $o) > $o), e : A]: ((('const/set_relation/per' A) xs xss) => (('const/set_relation/per' A) (('const/pred_set/DELETE' A) xs e) (('const/pred_set/GSPEC' (A > $o) (A > $o)) (^[es : (A > $o)]: (('const/pair/,' (A > $o) $o) es ((('const/bool/IN' (A > $o)) es (('const/pred_set/IMAGE' (A > $o) (A > $o)) (^[es0 : (A > $o)]: (('const/pred_set/DELETE' A) es0 e)) xss)) & (~ (es = ('const/pred_set/EMPTY' A))))))))))).
tt('thm/set_relation/per_restrict_per_', ax, ![A : $t]: (![r : ((A > $o) > $o), s : (A > $o), 's\'' : (A > $o)]: ((('const/set_relation/per' A) s r) => (('const/set_relation/per' A) 's\'' (('const/set_relation/per_restrict' A) r 's\''))))).
tt('thm/set_relation/countable_per_', ax, ![A : $t]: (![xs : (A > $o), xss : ((A > $o) > $o)]: (((('const/pred_set/countable' A) xs) & (('const/set_relation/per' A) xs xss)) => (('const/pred_set/countable' (A > $o)) xss)))).
tt('thm/set_relation/all_choices_def_', def, ![A : $t]: (![xss : ((A > $o) > $o)]: ((('const/set_relation/all_choices' A) xss) = (('const/pred_set/GSPEC' (A > $o) ((A > $o) > A)) (^[choice : ((A > $o) > A)]: (('const/pair/,' (A > $o) $o) (('const/pred_set/IMAGE' (A > $o) A) choice xss) (![xs : (A > $o)]: ((('const/bool/IN' (A > $o)) xs xss) => (('const/bool/IN' A) (choice xs) xs))))))))).
tt('thm/set_relation/all_choices_thm_', ax, ![A : $t]: (![x : (A > $o), s : ((A > $o) > $o), y : A]: (((('const/bool/IN' (A > $o)) x (('const/set_relation/all_choices' A) s)) & (('const/bool/IN' A) y x)) => (?[z : (A > $o)]: ((('const/bool/IN' (A > $o)) z s) & (('const/bool/IN' A) y z)))))).
tt('thm/set_relation/num_order_def_', def, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o)]: ((('const/set_relation/num_order' A) f s) = (('const/pred_set/GSPEC' ('type/pair/prod' A A) ('type/pair/prod' A A)) (('const/pair/UNCURRY' A A ('type/pair/prod' ('type/pair/prod' A A) $o)) (^[x : A, y : A]: (('const/pair/,' ('type/pair/prod' A A) $o) (('const/pair/,' A A) x y) ((('const/bool/IN' A) x s) & ((('const/bool/IN' A) y s) & ('const/arithmetic/<=' (f x) (f y))))))))))).
tt('thm/set_relation/linear_order_num_order_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o), t : ('type/num/num' > $o)]: ((('const/pred_set/INJ' A 'type/num/num') f s t) => (('const/set_relation/linear_order' A) (('const/set_relation/num_order' A) f s) s)))).
tt('thm/set_relation/num_order_finite_prefix_', ax, ![A : $t]: (![f : (A > 'type/num/num'), s : (A > $o), t : ('type/num/num' > $o)]: ((('const/pred_set/INJ' A 'type/num/num') f s t) => (('const/set_relation/finite_prefixes' A A) (('const/set_relation/num_order' A) f s) s)))).
tt('thm/set_relation/get_min_def_', def, ![A : $t]: (!['r\'' : (('type/pair/prod' A A) > $o), s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r)) = (('const/bool/LET' (A > $o) ('type/option/option' A)) (^[mins : (A > $o)]: (('const/bool/COND' ('type/option/option' A)) (('const/pred_set/SING' A) mins) (('const/option/SOME' A) (('const/pred_set/CHOICE' A) mins)) ('const/option/NONE' A))) (('const/set_relation/minimal_elements' A) (('const/set_relation/minimal_elements' A) s r) 'r\''))))).
tt('thm/set_relation/nth_min_tupled_primitive_def_', def, ![A : $t]: (('const/set_relation/nth_min_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) ('type/option/option' A)) (('const/min/@' (('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) > (('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) > $o))) (^[R : (('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) > (('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) > $o))]: ((('const/relation/WF' ('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num'))) R) & (![n : 'type/num/num', r : (('type/pair/prod' A A) > $o), s : (A > $o), 'r\'' : (('type/pair/prod' A A) > $o), min : ('type/option/option' A)]: (((min = (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r))) & (~ (min = ('const/option/NONE' A)))) => (R (('const/pair/,' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) 'r\'' (('const/pair/,' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num') (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) (('const/pred_set/DELETE' A) s (('const/option/THE' A) min)) r) n)) (('const/pair/,' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) 'r\'' (('const/pair/,' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num') (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) ('const/num/SUC' n))))))))) (^[nth_min_tupled : (('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) > ('type/option/option' A)), a : ('type/pair/prod' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num'))]: (('const/pair/pair_CASE' ('type/option/option' A) (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) a (^['r\'' : (('type/pair/prod' A A) > $o), v1 : ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')]: (('const/pair/pair_CASE' ('type/option/option' A) ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num') v1 (^[v2 : ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)), v3 : 'type/num/num']: (('const/pair/pair_CASE' ('type/option/option' A) (A > $o) (('type/pair/prod' A A) > $o)) v2 (^[s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (('const/arithmetic/num_CASE' ('type/option/option' A)) v3 (('const/combin/I' ('type/option/option' A)) (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r))) (^[n : 'type/num/num']: (('const/combin/I' ('type/option/option' A)) (('const/bool/LET' ('type/option/option' A) ('type/option/option' A)) (^[min : ('type/option/option' A)]: (('const/bool/COND' ('type/option/option' A)) (min = ('const/option/NONE' A)) ('const/option/NONE' A) (nth_min_tupled (('const/pair/,' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) 'r\'' (('const/pair/,' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num') (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) (('const/pred_set/DELETE' A) s (('const/option/THE' A) min)) r) n))))) (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r)))))))))))))))).
tt('thm/set_relation/nth_min_curried_def_', def, ![A : $t]: (![x : (('type/pair/prod' A A) > $o), x1 : ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)), x2 : 'type/num/num']: ((('const/set_relation/nth_min' A) x x1 x2) = (('const/set_relation/nth_min_tupled' A) (('const/pair/,' (('type/pair/prod' A A) > $o) ('type/pair/prod' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num')) x (('const/pair/,' ('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) 'type/num/num') x1 x2)))))).
tt('thm/set_relation/nth_min_ind_', ax, ![A : $t]: (![P : ((('type/pair/prod' A A) > $o) > (('type/pair/prod' (A > $o) (('type/pair/prod' A A) > $o)) > ('type/num/num' > $o)))]: (((!['r\'' : (('type/pair/prod' A A) > $o), s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (P 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) 'const/num/0')) & (!['r\'' : (('type/pair/prod' A A) > $o), s : (A > $o), r : (('type/pair/prod' A A) > $o), n : 'type/num/num']: ((![min : ('type/option/option' A)]: (((min = (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r))) & (~ (min = ('const/option/NONE' A)))) => (P 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) (('const/pred_set/DELETE' A) s (('const/option/THE' A) min)) r) n))) => (P 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) ('const/num/SUC' n))))) => (![v : (('type/pair/prod' A A) > $o), v1 : (A > $o), v2 : (('type/pair/prod' A A) > $o), v3 : 'type/num/num']: (P v (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) v1 v2) v3))))).
tt('thm/set_relation/nth_min_def_0', ax, ![A : $t]: (![s : (A > $o), 'r\'' : (('type/pair/prod' A A) > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) 'const/num/0') = (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r))))).
tt('thm/set_relation/nth_min_def_e1', ax, ![A : $t]: (![s : (A > $o), 'r\'' : (('type/pair/prod' A A) > $o), r : (('type/pair/prod' A A) > $o), n : 'type/num/num']: ((('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) ('const/num/SUC' n)) = (('const/bool/LET' ('type/option/option' A) ('type/option/option' A)) (^[min : ('type/option/option' A)]: (('const/bool/COND' ('type/option/option' A)) (min = ('const/option/NONE' A)) ('const/option/NONE' A) (('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) (('const/pred_set/DELETE' A) s (('const/option/THE' A) min)) r) n))) (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r)))))).
tt('thm/set_relation/nth_min_def_compute_0', ax, ![A : $t]: (![s : (A > $o), 'r\'' : (('type/pair/prod' A A) > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) 'const/num/0') = (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r))))).
tt('thm/set_relation/nth_min_def_compute_1', ax, ![A : $t]: (![s : (A > $o), 'r\'' : (('type/pair/prod' A A) > $o), r : (('type/pair/prod' A A) > $o), n : 'type/num/num']: ((('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = (('const/bool/LET' ('type/option/option' A) ('type/option/option' A)) (^[min : ('type/option/option' A)]: (('const/bool/COND' ('type/option/option' A)) (min = ('const/option/NONE' A)) ('const/option/NONE' A) (('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) (('const/pred_set/DELETE' A) s (('const/option/THE' A) min)) r) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r)))))).
tt('thm/set_relation/nth_min_def_compute_e2', ax, ![A : $t]: (![s : (A > $o), 'r\'' : (('type/pair/prod' A A) > $o), r : (('type/pair/prod' A A) > $o), n : 'type/num/num']: ((('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = (('const/bool/LET' ('type/option/option' A) ('type/option/option' A)) (^[min : ('type/option/option' A)]: (('const/bool/COND' ('type/option/option' A)) (min = ('const/option/NONE' A)) ('const/option/NONE' A) (('const/set_relation/nth_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) (('const/pred_set/DELETE' A) s (('const/option/THE' A) min)) r) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) (('const/set_relation/get_min' A) 'r\'' (('const/pair/,' (A > $o) (('type/pair/prod' A A) > $o)) s r)))))).
tt('thm/set_relation/linear_order_of_countable_po_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o), s : (A > $o)]: (((('const/pred_set/countable' A) s) & ((('const/set_relation/partial_order' A) r s) & (('const/set_relation/finite_prefixes' A A) r s))) => (?['r\'' : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/linear_order' A) 'r\'' s) & ((('const/set_relation/finite_prefixes' A A) 'r\'' s) & (('const/pred_set/SUBSET' ('type/pair/prod' A A)) r 'r\''))))))).
tt('thm/set_relation/reln_to_rel_def_', def, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/reln_to_rel' A B) r) = (^[x : A, y : B]: (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) r))))).
tt('thm/set_relation/rel_to_reln_def_', def, ![B : $t, A : $t]: (![R : (A > (B > $o))]: ((('const/set_relation/rel_to_reln' A B) R) = (('const/pred_set/GSPEC' ('type/pair/prod' A B) ('type/pair/prod' A B)) (('const/pair/UNCURRY' A B ('type/pair/prod' ('type/pair/prod' A B) $o)) (^[x : A, y : B]: (('const/pair/,' ('type/pair/prod' A B) $o) (('const/pair/,' A B) x y) (R x y)))))))).
tt('thm/set_relation/RRUNIV_def_', def, ![A : $t]: (![s : (A > $o)]: ((('const/set_relation/RRUNIV' A) s) = (^[x : A, y : A]: ((('const/bool/IN' A) x s) & (('const/bool/IN' A) y s)))))).
tt('thm/set_relation/RREFL_EXP_def_', def, ![A : $t]: (![R : (A > (A > $o)), s : (A > $o)]: ((('const/set_relation/RREFL_EXP' A) R s) = (('const/relation/RUNION' A A) R (^[x : A, y : A]: ((x = y) & (~ (('const/bool/IN' A) x s)))))))).
tt('thm/set_relation/RREFL_EXP_RSUBSET_', ax, ![A : $t]: (![s : (A > $o), R : (A > (A > $o))]: (('const/relation/RSUBSET' A A) R (('const/set_relation/RREFL_EXP' A) R s)))).
tt('thm/set_relation/RREFL_EXP_UNIV_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/set_relation/RREFL_EXP' A) R ('const/pred_set/UNIV' A)) = R))).
tt('thm/set_relation/REL_RESTRICT_UNIV_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/pred_set/REL_RESTRICT' A) R ('const/pred_set/UNIV' A)) = R))).
tt('thm/set_relation/in_rel_to_reln_', ax, ![A : $t, B : $t]: (![xy : ('type/pair/prod' A B), R : (A > (B > $o))]: ((('const/bool/IN' ('type/pair/prod' A B)) xy (('const/set_relation/rel_to_reln' A B) R)) = (R (('const/pair/FST' A B) xy) (('const/pair/SND' A B) xy))))).
tt('thm/set_relation/reln_to_rel_app_', ax, ![A : $t, B : $t]: (![y : B, x : A, r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/reln_to_rel' A B) r x y) = (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) r)))).
tt('thm/set_relation/rel_to_reln_inv_', ax, ![A : $t, B : $t]: (![R : (A > (B > $o))]: ((('const/set_relation/reln_to_rel' A B) (('const/set_relation/rel_to_reln' A B) R)) = R))).
tt('thm/set_relation/reln_to_rel_inv_', ax, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/rel_to_reln' A B) (('const/set_relation/reln_to_rel' A B) r)) = r))).
tt('thm/set_relation/reln_to_rel_11_', ax, ![A : $t, B : $t]: (![r2 : (('type/pair/prod' A B) > $o), r1 : (('type/pair/prod' A B) > $o)]: (((('const/set_relation/reln_to_rel' A B) r1) = (('const/set_relation/reln_to_rel' A B) r2)) = (r1 = r2)))).
tt('thm/set_relation/rel_to_reln_11_', ax, ![A : $t, B : $t]: (![R2 : (A > (B > $o)), R1 : (A > (B > $o))]: (((('const/set_relation/rel_to_reln' A B) R1) = (('const/set_relation/rel_to_reln' A B) R2)) = (R1 = R2)))).
tt('thm/set_relation/rel_to_reln_swap_', ax, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o), R : (A > (B > $o))]: ((r = (('const/set_relation/rel_to_reln' A B) R)) = ((('const/set_relation/reln_to_rel' A B) r) = R)))).
tt('thm/set_relation/domain_to_rel_conv_', ax, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/domain' A B) r) = (('const/relation/RDOM' A B) (('const/set_relation/reln_to_rel' A B) r))))).
tt('thm/set_relation/range_to_rel_conv_', ax, ![B : $t, A : $t]: (![r : (('type/pair/prod' B A) > $o)]: ((('const/set_relation/range' A B) r) = (('const/relation/RRANGE' B A) (('const/set_relation/reln_to_rel' B A) r))))).
tt('thm/set_relation/strict_to_rel_conv_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/strict' A) r) = (('const/set_relation/rel_to_reln' A A) (('const/relation/STRORD' A) (('const/set_relation/reln_to_rel' A A) r)))))).
tt('thm/set_relation/rcomp_to_rel_conv_', ax, ![A : $t, C : $t, B : $t]: (![r2 : (('type/pair/prod' C B) > $o), r1 : (('type/pair/prod' A C) > $o)]: ((('const/set_relation/rcomp' A B C) r1 r2) = (('const/set_relation/rel_to_reln' A B) (('const/relation/O' A C B) (('const/set_relation/reln_to_rel' C B) r2) (('const/set_relation/reln_to_rel' A C) r1)))))).
tt('thm/set_relation/rrestrict_to_rel_conv_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/set_relation/univ_reln' A) s) = (('const/set_relation/rel_to_reln' A A) (('const/set_relation/RRUNIV' A) s))))).
tt('thm/set_relation/tc_to_rel_conv_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/tc' A) r) = (('const/set_relation/rel_to_reln' A A) (('const/relation/TC' A) (('const/set_relation/reln_to_rel' A A) r)))))).
tt('thm/set_relation/acyclic_reln_to_rel_conv_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/acyclic' A) r) = (('const/relation/irreflexive' A) (('const/relation/TC' A) (('const/set_relation/reln_to_rel' A A) r)))))).
tt('thm/set_relation/irreflexive_reln_to_rel_conv_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/irreflexive' A) r s) = (('const/relation/irreflexive' A) (('const/pred_set/REL_RESTRICT' A) (('const/set_relation/reln_to_rel' A A) r) s))))).
tt('thm/set_relation/irreflexive_reln_to_rel_conv_UNIV_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/irreflexive' A) r ('const/pred_set/UNIV' A)) = (('const/relation/irreflexive' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reflexive_reln_to_rel_conv_UNIV_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/reflexive' A) r ('const/pred_set/UNIV' A)) = (('const/relation/reflexive' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reflexive_reln_to_rel_conv_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/transitive' A) r) = (('const/relation/transitive' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/antisym_reln_to_rel_conv_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/antisym' A) r) = (('const/relation/antisymmetric' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/partial_order_reln_to_rel_conv_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/partial_order' A) r s) = ((('const/relation/RSUBSET' A A) (('const/set_relation/reln_to_rel' A A) r) (('const/set_relation/RRUNIV' A) s)) & (('const/relation/WeakOrder' A) (('const/set_relation/RREFL_EXP' A) (('const/set_relation/reln_to_rel' A A) r) s)))))).
tt('thm/set_relation/partial_order_reln_to_rel_conv_UNIV_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/partial_order' A) r ('const/pred_set/UNIV' A)) = (('const/relation/WeakOrder' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/linear_order_reln_to_rel_conv_UNIV_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/linear_order' A) r ('const/pred_set/UNIV' A)) = (('const/relation/WeakLinearOrder' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/strict_linear_order_reln_to_rel_conv_UNIV_', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/strict_linear_order' A) r ('const/pred_set/UNIV' A)) = (('const/relation/StrongLinearOrder' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reln_rel_conv_thms_tLL', ax, ![A : $t, B : $t]: (![xy : ('type/pair/prod' A B), R : (A > (B > $o))]: ((('const/bool/IN' ('type/pair/prod' A B)) xy (('const/set_relation/rel_to_reln' A B) R)) = (R (('const/pair/FST' A B) xy) (('const/pair/SND' A B) xy))))).
tt('thm/set_relation/reln_rel_conv_thms_tLRL', ax, ![A : $t, B : $t]: (![y : B, x : A, r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/reln_to_rel' A B) r x y) = (('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) r)))).
tt('thm/set_relation/reln_rel_conv_thms_tLRRL', ax, ![A : $t, B : $t]: (![R : (A > (B > $o))]: ((('const/set_relation/reln_to_rel' A B) (('const/set_relation/rel_to_reln' A B) R)) = R))).
tt('thm/set_relation/reln_rel_conv_thms_tLRRRL', ax, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/rel_to_reln' A B) (('const/set_relation/reln_to_rel' A B) r)) = r))).
tt('thm/set_relation/reln_rel_conv_thms_tLRRRRL', ax, ![A : $t, B : $t]: (![r2 : (('type/pair/prod' A B) > $o), r1 : (('type/pair/prod' A B) > $o)]: (((('const/set_relation/reln_to_rel' A B) r1) = (('const/set_relation/reln_to_rel' A B) r2)) = (r1 = r2)))).
tt('thm/set_relation/reln_rel_conv_thms_tRRRRRL', ax, ![A : $t, B : $t]: (![R2 : (A > (B > $o)), R1 : (A > (B > $o))]: (((('const/set_relation/rel_to_reln' A B) R1) = (('const/set_relation/rel_to_reln' A B) R2)) = (R1 = R2)))).
tt('thm/set_relation/reln_rel_conv_thms_1', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/set_relation/RREFL_EXP' A) R ('const/pred_set/UNIV' A)) = R))).
tt('thm/set_relation/reln_rel_conv_thms_2', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/pred_set/REL_RESTRICT' A) R ('const/pred_set/UNIV' A)) = R))).
tt('thm/set_relation/reln_rel_conv_thms_3', ax, ![A : $t, B : $t]: (![r : (('type/pair/prod' A B) > $o)]: ((('const/set_relation/domain' A B) r) = (('const/relation/RDOM' A B) (('const/set_relation/reln_to_rel' A B) r))))).
tt('thm/set_relation/reln_rel_conv_thms_4', ax, ![B : $t, A : $t]: (![r : (('type/pair/prod' B A) > $o)]: ((('const/set_relation/range' A B) r) = (('const/relation/RRANGE' B A) (('const/set_relation/reln_to_rel' B A) r))))).
tt('thm/set_relation/reln_rel_conv_thms_5', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/strict' A) r) = (('const/set_relation/rel_to_reln' A A) (('const/relation/STRORD' A) (('const/set_relation/reln_to_rel' A A) r)))))).
tt('thm/set_relation/reln_rel_conv_thms_6', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/rrestrict' A) r s) = (('const/set_relation/rel_to_reln' A A) (('const/pred_set/REL_RESTRICT' A) (('const/set_relation/reln_to_rel' A A) r) s))))).
tt('thm/set_relation/reln_rel_conv_thms_7', ax, ![A : $t, C : $t, B : $t]: (![r2 : (('type/pair/prod' C B) > $o), r1 : (('type/pair/prod' A C) > $o)]: ((('const/set_relation/rcomp' A B C) r1 r2) = (('const/set_relation/rel_to_reln' A B) (('const/relation/O' A C B) (('const/set_relation/reln_to_rel' C B) r2) (('const/set_relation/reln_to_rel' A C) r1)))))).
tt('thm/set_relation/reln_rel_conv_thms_8', ax, ![A : $t]: (![s : (A > $o)]: ((('const/set_relation/univ_reln' A) s) = (('const/set_relation/rel_to_reln' A A) (('const/set_relation/RRUNIV' A) s))))).
tt('thm/set_relation/reln_rel_conv_thms_9', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/tc' A) r) = (('const/set_relation/rel_to_reln' A A) (('const/relation/TC' A) (('const/set_relation/reln_to_rel' A A) r)))))).
tt('thm/set_relation/reln_rel_conv_thms_10', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/acyclic' A) r) = (('const/relation/irreflexive' A) (('const/relation/TC' A) (('const/set_relation/reln_to_rel' A A) r)))))).
tt('thm/set_relation/reln_rel_conv_thms_11', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/irreflexive' A) r s) = (('const/relation/irreflexive' A) (('const/pred_set/REL_RESTRICT' A) (('const/set_relation/reln_to_rel' A A) r) s))))).
tt('thm/set_relation/reln_rel_conv_thms_12', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/reflexive' A) r s) = (('const/relation/reflexive' A) (('const/set_relation/RREFL_EXP' A) (('const/set_relation/reln_to_rel' A A) r) s))))).
tt('thm/set_relation/reln_rel_conv_thms_13', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/transitive' A) r) = (('const/relation/transitive' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reln_rel_conv_thms_14', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/antisym' A) r) = (('const/relation/antisymmetric' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reln_rel_conv_thms_15', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/partial_order' A) r ('const/pred_set/UNIV' A)) = (('const/relation/WeakOrder' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reln_rel_conv_thms_16', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/linear_order' A) r ('const/pred_set/UNIV' A)) = (('const/relation/WeakLinearOrder' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/reln_rel_conv_thms_e17', ax, ![A : $t]: (![r : (('type/pair/prod' A A) > $o)]: ((('const/set_relation/strict_linear_order' A) r ('const/pred_set/UNIV' A)) = (('const/relation/StrongLinearOrder' A) (('const/set_relation/reln_to_rel' A A) r))))).
tt('thm/set_relation/acyclic_WF_', ax, ![A : $t]: (![s : (A > $o), r : (('type/pair/prod' A A) > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/set_relation/acyclic' A) r) & ((('const/pred_set/SUBSET' A) (('const/set_relation/domain' A A) r) s) & (('const/pred_set/SUBSET' A) (('const/set_relation/range' A A) r) s)))) => (('const/relation/WF' A) (('const/set_relation/reln_to_rel' A A) r))))).
