Nuprl - Proof: fun exp compose 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp compose 2

1. T : Type
2. n :

3. 0<n
4.

h,f:(T

T). f^n-1 o h = primrec(n-1;h;

i,g. f o g)

h,f:(T

T). primrec(n;

x.x;

i,g. f o g) o h = primrec(n;h;

i,g. f o g)

By:	Auto THEN Subst' (n = 1+n-1) 0

Generated subgoal:

1 5. h : TT
6. f : TT
primrec(1+n-1;x.x;i,g. f o g) o h = primrec(1+n-1;h;i,g. f o g)
8 steps

About:

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