Def  == {i:| 0<i }

is mentioned by

Thm* Size(Cons(Inj(1);Cons(Inj(2);Inj(1)))) = 3	[sfa_doc_sexpr_size_example]
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* A:Type, s:Sexpr(A). Size(s)	[sfa_doc_sexpr_size_wf]

In prior sections: int 1 int 2

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