(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp compose 2 1 1 2

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


By: Fold `fun_exp` 0 THEN Subst (f o f^n-1 o h = f o f^n-1 o h) 0


Generated subgoals:

1   f o f^n-1 o h = f o f^n-1 o h
1 step
2   f o f^n-1 o h = f o primrec(n-1;h;i,gf o g)
2 steps

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

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