is mentioned by

Thm*  A:Type, a:A, xs:A List. (a  xs)  Prop	[is_list_mem_wf]
Thm*  same_range_sep(A; B)  (A inj B)(A inj B)Prop	[same_range_sep_wf_inj]
Thm*  same_range_sep(A; B)  (AB)(AB)Prop	[same_range_sep_wf]
Thm*  f:(a2).  Thm*  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f)))	[card_st_vs_msize]
Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))	[card_split_decbl_squash]
Thm*  B:(AType), P:(AProp). Thm*  (i:A. Dec(P(i))) Thm*   Thm*  ((i:AB(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i))))	[card_split_sigma_dom_decbl]
Thm*  B:(AType), P:(AProp). Thm*  (i:{i:A| P(i) }B(i)) ~ {v:(i:AB(i))| P(v/x,y. x) }	[card_sigma_st_dom]
Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))	[card_split_decbl]
Thm*  (q:A/E{x:A| q = x  A/E }) ~ A	[card_quotient]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })	[set_functionality_wrt_one_one_corr_n_pred]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })	[set_functionality_wrt_one_one_corr_n_pred2]
Thm*  Bij(A; A'; f) Thm*   Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })	[card_settype_sq]
Thm*  Bij(A; A'; f) Thm*   Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })	[card_settype]
Thm*  P:(ABProp). (x:A. !y:B. P(x;y))  (A ~ (y:B{x:A| P(x;y) }))	[partition_type]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P)	[nonfin_eqv_unb_inf_iff_negnegelim]
Thm*  (P:Prop. P  P)  (A:Type. Finite(A)  Unbounded(A))	[negnegelim_imp_notfin_imp_unb_inf]
Thm*  (A  C)  (B  D)  A & B  C & D	[parallel_conjunct_imp]
Thm*  k:, B:(kType), Q:(x:kB(x)Prop). Thm*  (x:k. y:B(x). Q(x;y))  (f:(x:kB(x)). x:k. Q(x;f(x)))	[dep_finite_choice]
Thm*  k:, Q:(kAProp). Thm*  (x:k. y:A. Q(x;y))  (f:(kA). x:k. Q(x;f(x)))	[finite_choice]
Thm*  (x:A. Dec(P(x))) Thm*   Thm*  ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x))))	[card_split_prod_intseg_family_decbl]
Thm*  R:(ABProp).  Thm*  (1-1-Corr x:A,y:B. R(x;y)) Thm*   Thm*  (f:(AB), g:(BA). Thm*  (InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y)))	[one_one_corr_rel_vs_invfuns]
Thm*  A:Type. Dedekind-Infinite(A)  Prop	[Dedekind_infinite_wf]
Thm*  A:Type. Infinite(A)  Prop	[productively_infinite_wf]
Thm*  A:Type. Unbounded(A)  Prop	[unboundedly_infinite_wf]
Thm*  P:{P:(Prop)| i:. P(i) }.  Thm*  (i:. Dec(P(i)))  ({i:| P(i) & (j:. j<i  P(j)) })	[least_exists2]
Thm*  k:, P:{P:(kProp)| i:k. P(i) }. Thm*  (i:k. Dec(P(i)))  ({i:k| P(i) & (j:i. P(j)) })	[least_exists]
Thm*  Dec(P)  (!i:2. if i=0 P else P fi)	[decidable_vs_unique_nsub2]
Thm*  A:Type, A':Type, B:(AType), B':(A'Type). Thm*  ((x:A. B(x)) ~ (x':A'. B'(x')))  Prop	[one_one_corr_fams_wf]
Thm*  {x:A| B(x) } ~ {x:A| B(x) }	[subset_sq_remove_card]
Thm*  {x:{x:A| P(x) }| Q(x) } ~ {x:A| P(x) & Q(x) }	[card_subset_vs_and]
Thm*  {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype_ooc]
Thm*  (A:Type, R:(AAProp). Thm*  ((A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*  (& (x:A. R(x;x)) Thm*  (& Finite(A))	[no_finite_model]
Thm*  R:(AAProp).  Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*   Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))	[no_finite_model_lemma]
Thm*  A:Type. Finite(A)  Prop	[is_finite_type_wf]
Thm*  A = A'  B = B'  (A ~ B) = (A' ~ B')	[one_one_corr_2_functionality_wrt_eq]
Thm*  A,B:Type. (A ~ B)  Prop	[one_one_corr_2_wf]
Thm*  R:(ABProp). (R is 1-1) = (1-1 xA,yB. R(x;y))	[rel_1_1_eq_rel_1_1_b]
Thm*  A,B:Type, R:(ABProp). (R is 1-1)  Type	[rel_1_1_wf]
Thm*  Bij({u:| P(u) }; {v:| Q(v) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }. Thm*  (Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k }; Thm*  (Bij(Replace value k by f(m) in f))	[delete_fenum_value_is_fenum_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }. Thm*  (Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k }; Thm*  (Inj(Replace value k by f(m) in f))	[delete_fenum_value_is_inj_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }. Thm*  ((Replace value k by f(m) in f) Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k } Thm*  (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k }; Thm*  (& Inj(Replace value k by f(m) in f))	[delete_fenum_value_is_inj_genW]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }. Thm*  (f(i) = k Thm*  ( Thm*  ((Replace value k by f(m) in f)(i) = f(i)  {v:| Q(v) & v = k })	[delete_fenum_value_comp2_gen]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }. Thm*  (f(i) = k Thm*  ( Thm*  ((Replace value k by f(m) in f)(i) = f(m)  {v:| Q(v) & v = k })	[delete_fenum_value_comp1_gen]
Thm*  Inj({k:| P(k) }; {k:| Q(k) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }. Thm*  ((Replace value k by f(m) in f) Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k })	[delete_fenum_value_wf_gen]
Thm*  A,B:Type, R:(ABProp). (1-1-Corr x:A,y:B. R(x;y))  Prop	[is_one_one_corr_rel_wf]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html