n,i:. (i  upto(n))  i<n

By:	Auto THEN All (Unfold `l_member`) THEN ExRepD THEN Try (InstConcl [i]) THEN All (RWO Thm* n:. ||upto(n)|| ~ n) THEN Try (Inst Thm* m:, n:m. upto(m)[n] = n [n;i] THEN Complete Auto) THEN Try (Inst Thm* m:, n:m. upto(m)[n] = n [n;i@0] THEN Complete Auto)

None

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