Def A^n == if n=0 Unit ; n=1 A else A(A^(n-1)) fi  (recursive)

is mentioned by

Thm* A:Type, P:(AProp), n:, X:(A^n). ( u in X: A^n. P(u))  Prop	[sfa_doc_ntuple_contains_wf]
Thm* n:. n2  (A^n) = A(A^(n-1))	[sfa_doc_ntuple_is_prod]

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