Nuprl Basics - Proof: sfa doc sample intmod wf 1 3 1

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

1. k :

2. a :

3. b :

4. c :

. a-b = m

k
6.

. b-c = m

. a-c = m

By:	Analyze-2 THEN Analyze-1

Generated subgoal:

1 5. m :
6. a-b = mk
7. m1 :
8. b-c = m1k
m:. a-c = mk
1 step

About:

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