(4steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: primrec wf 2 1

1. T : Type
2. n : 
3. 0<n
4. b:Tc:((n-1)TT). primrec(n-1;b;c T
5. b : T
6. c : nTT
7. n = 0
  primrec(n-1;b;c T


By: BackThruSomeHyp


Generated subgoals:

None

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

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