(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp compose
  T:Type, n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g)
By: RepeatFor 2 (Analyze 0) THEN NatInd -1 THEN Unfold `fun_exp` 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
  h,f:(TT). (x.x) o h = h
1 step
2 1. T : Type
2. n : 
3. 0<n
4. h,f:(TT). f^n-1 o h = primrec(n-1;h;i,g. f o g)
  h,f:(TT). primrec(n;x.x;i,g. f o g) o h = primrec(n;h;i,g. f o g)
9 steps

About:
lambdafunctionuniverseequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Search Doc