Def  P  Q == (P  Q) & (P  Q)

is mentioned by

Thm*  (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))	[ax_choice_version3]
Thm*  f,g:(AB). f = g  (x:A. f(x) = g(x))	[indep_fun_extensional]
Thm*  (!A)  (!x:A. True)	[inhabited_uniquely_vs_exists_unique]
Thm*  P:(AType). (x:A. Dec(P(x)))  (!{p:(A)| x:A. p(x)  P(x) })	[dec_pred_imp_bool_decider_exists]
Thm*  (x:T. Dec(E(x)))  (f:(T). x:T. f(x)  E(x))	[dec_pred_iff_some_boolfun]
Thm*  R:(AAProp).  Thm*  (EquivRel x,y:A. R(x,y)) Thm*   Thm*  (x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z))))	[equivrel_characterization]
Thm*  (Set:Type, :(SetSetProp). Thm*  (P:(SetProp). p:Set. x:Set. (x  p)  P(x))	[RussellsParadox_Frege2]
Thm*  (A:Type, Q:(AAProp). P:(AProp). p:A. x:A. Q(x,p)  P(x))	[RussellsParadox_Frege]
Thm*  (P  P)	[no_prop_iff_its_neg]
Thm*  (A Discrete)  (e:(AA). IsEqFun(A;e))	[discrete_vs_bool2]
Thm*  (A Discrete)  (e:(AA). x,y:A. (x e y)  x = y)	[discrete_vs_bool]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_sq_exteq]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_exteq]
Thm*  P XOR Q  (Q  P) & Dec(P)	[xor_vs_neg_n_dec]
Thm*  P  P	[sq_sq_iff_sq]
Thm*  (P)  P	[sq_not_iff_sq]
Thm*  P  P	[not_sq_iff_sq]
Thm*  (!A)  (x:A. y:A. x = y)	[inhabited_uniquely_vs_exists]
Thm*  (A)  (x:A. True)	[inhabited_vs_exists]
Thm*  F:(PropProp). (P:Prop. F(P))  (A:Type. F(A))	[inhab_rep_eqv]
Thm*  (x:A. B(x))  ((x:AB(x)))	[inhab_choice]
Thm*  Dec(P)  (b:. b  P)	[decbl_iff_some_bool]
Thm*  Q  Q  Q	[or_fused]
Thm*  (P:Prop. P  P)  (P:Prop. P  P)	[negnegelim_vs_bivalence]

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

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