IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
strict part irrefl1 1. T : Type
2. R : TTProp
3. a : T 4. b : T 5. R(a,b)
6. R(b,a)
7. a = b False
By:
OnHyps [5;6] (HypSubst 7)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
R(b,a)
False
