(4steps 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 add1

  T:Type, f:(TT), n:x:Tf(f^n(x)) = f^n+1(x)

By: Auto THEN Subst (f^n+1 = f o f^n) 0 THEN Reduce 0


Generated subgoal:

1 1. T : Type
2. f : TT
3. n : 
4. T
  f^n+1 = f o f^n

3 steps

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

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