(11steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: concat map upto 2 1 1
1. T : Type
2. (T List)
3. t : 
4. t' : 
5. t<t'
  upto(t+1)  upto(t')
By: BackThru Thm* i,j:. ij  upto(i)  upto(j)

Generated subgoals:

None

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

(11steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc