IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fun exp compose21121 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)
5. h : TT 6. f : TT f o f^n-1 o h = f o f^n-1 o h
By:
Ext THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
h,f:(T
T). f^n-1 o h = primrec(n-1;h;
i,g. f o g)
f o f^n-1 o h = f o f^n-1 o h
