1. T : Type
2. n : 
3. 0<n
4. b:T, c:((n-1)TT). primrec(n-1;b;c)  T
5. b : T
6. c : nTT
  if n=0 b else c(n-1,primrec(n-1;b;c)) fi  T

1

7. n = 0   primrec(n-1;b;c)  T

1 step

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