1. a : 
2. b : 
3. y : 
4. k : 
5. y | a
6. y | b
7. z:. z | a & z | b  z | y
8. z : 
9. z | a
10. z | b+ka
  z | b+ka+a(-k)

By:	BackThru Thm* a,b1,b2:. a | b1  a | b2  a | b1+b2

1	z | b+ka	Hypothesis
2	z | a(-k)	1 step

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