Def P  Q == PQ

is mentioned by

Thm* f:(D:Type. D(D List)), A:Type, a,x:A. x list f(a)  x = a	[sfa_doc_type_poly_mem_const]
Thm* a:A, w:{a:A} List. z:A. z list w  z = a	[sfa_doc_inlist_singleton_const]
Thm* P:(AProp). (x:A. Dec(P(x)))  (f:(A). x:A. P(x)  f(x))	[sfa_doc_bool_vs_decidable_fun]
Thm* f,g:(). Thm* (x:. f zero beyond x) & (x:. g zero beyond x) Thm*  Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x)	[sfa_doc_alternate_zero_beyond]
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))	[sfa_doc_or_dec]
Thm* f:().  Thm* (n:. f(n) = 0) Thm*  Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi)  Prop{1}	[sfa_doc_predicativity_sample8]
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* (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]
Thm* A:Prop, B:Prop(given A). (A  B)  Prop	[sfa_doc_imp_typing]
Thm* A:Type, s:Sexpr(A). Size(s) = 1    sexprAtom(s)  A	[sfa_doc_sexpr_atom_wf]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCdr(s))<Size(s)	[sfa_doc_sexprcdrsize]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCar(s))<Size(s)	[sfa_doc_sexprcarsize]
Thm* n:. n2  (A^n) = A(A^(n-1))	[sfa_doc_ntuple_is_prod]
Thm* k:. 0<k & (2  k)<1  2<k	[sfa_doc_cand_example]
Thm* f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)	[kleene_minimize_is_lb]
Thm* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) }	[kleene_tail]
Def f zero beyond x == y:. x<y  f(y) = 0	[sfa_doc_props_as_types_example1]
Def HigherConsequence{i}(P) == {X:Prop{i'}| P  X }	[sfa_doc_le_parm_sample_def]
Def Induction for x:. P(x) == P(0) & (x:. P(x)  P(x+1))  (x:. P(x))	[sfa_doc_indscheme]

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

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