Nuprl - Proof: fun exp add1 1 1 1

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

1. T : Type
2. f : T

T
3. n :

4. T
5. f^1+n = f^1 o f^n

f^1 o f^n = f o f^n

By:	Ext THEN Reduce 0

Generated subgoals:

None

About:

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