(3steps total) PrintForm Definitions mb event system 7 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable rset equal
  R:(Id), x,y:|R|. Dec(x = y)
By: Unfold `rset` 0 THEN Analyze -2 THEN Analyze -1 THEN Assert Dec(x = y)
THEN
RepeatFor 2 (ParallelOp -1)
THEN
Unhide

Generated subgoals:

1 1. R : Id
2. x : Id
3. R(x)
4. y : Id
5. R(y)
6. x = y
  x = y  {i:Id| R(i) }
1 step
2 1. R : Id
2. x : Id
3. R(x)
4. y : Id
5. R(y)
6. x = y
  x = y  {i:Id| R(i) }
1 step

About:
boolassertdecidablesetapplyfunctionequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(3steps total) PrintForm Definitions mb event system 7 Sections EventSystems Search Doc