(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 1
1. T : Type
2. f : (T List)
3. t : 
4. t' : 
5. t<t'
  (concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t+1)))
By: RW (AddrC [2] (RecUnfoldC `upto`)) 0 THEN SplitOnConclITE

Generated subgoals:

1 6. t+1 = 0
  (concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;nil))
Auto
2 6. t+1 = 0
  (concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t+1-1) @ [(t+1-1)]))
5 steps

About:
listconsnilnatural_numberaddsubtractless_thanapplyfunctionuniversesqequal
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