Nuprl - Proof: member upto2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: member upto2

n,i:

. i<n

upto(n))

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

Generated subgoals:

None

About:

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