(3steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel rel star 1 1
1. T : Type
2. R : TTProp
3. x : T
4. y : T
5. x R y
  x R^1 y
By: RepeatFor 2 (RecUnfold `rel_exp` 0 THEN Reduce 0) THEN SimpConcl

Generated subgoals:

None

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

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