Nuprl Basics - Proof: sfa doc sample intmod wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sample intmod wf 1

1. k :

EquivRel x,y:

. x-y = m

By:

Def

Generated subgoals:

1   Refl(;x,y.m:. x-y = mk)
2 steps

2   Sym x,y:. m:. x-y = mk
2 steps

3   Trans x,y:. m:. x-y = mk
3 steps

About:

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