1. A : Type
2. n : 
3. n1:. n1<n  (A^n1)  Type
  (A^n)  Type

By:	Compute A^n * if n=0 Unit ; n=1 A else A(A^(n-1)) fi THEN SplitITE Concl THENL [Id;SplitITE Concl]

1	4. n = 0   Unit  Type	Auto
2	4. n  0 5. n = 1   A  Type	Trivial
3	4. n  0 5. n  1   A(A^(n-1))  Type	3 steps

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