Def  u in X: A^n. P(u)
Def == n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u)))
Def (recursive)

is mentioned by

Thm*  i in <1,(-1),0>: ^3. i<0

[sfa_doc_ntuple_contains_example]

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