IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
primrec add11 1. T : Type
2. m : 3. b : T 4. c : (0+m)TT primrec(0+m;b;c) = primrec(m;b;c)
By:
Subst' (0+m = m) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
primrec(0+m;b;c) = primrec(m;b;c)
