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

is mentioned by

Thm* f,g:(AB). f = g  (x:A. f(x) = g(x))	[sfa_doc_fun_ext]
Thm* P:(AProp). (x:A. Dec(P(x)))  (f:(A). x:A. P(x)  f(x))	[sfa_doc_bool_vs_decidable_fun]
Thm* Dec(P)  (b:. P  b)	[sfa_doc_bool_vs_decidable]
Thm* R:(A(A List)PropProp).  Thm* P:((A List)Prop).  Thm* (P(nil)  Q) & (a:A, x:A List. P(a.x)  R(a,x,P(x)))	[sfa_doc_listind_via_so]
Thm* a,b:A. a = b  (P:(AProp). P(a)  P(b))	[sfa_doc_equal_via_so]
Thm* B:(AProp). (x:A. B(x))  (C:Prop. (x:A. B(x)  C)  C)	[sfa_doc_some_via_so]
Thm* False  (C:Prop. C)	[sfa_doc_false_via_so]
Thm* (A  B)  (C:Prop. ((A  B)  (B  A)  C)  C)	[sfa_doc_iff_via_so]
Thm* A  (C:Prop. A  C)	[sfa_doc_not_via_so]
Thm* A  B  (C:Prop. (A  C)  (B  C)  C)	[sfa_doc_or_via_so]
Thm* A & B  (C:Prop. (A  B  C)  C)	[sfa_doc_and_via_so]

In prior sections: core well fnd int 1 bool 1 rel 1 fun 1 int 2 list 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html