1. a : 
2. b : 
3. y : 
4. k : 
5. y | a
6. y | b
7. z:. z | a & z | b  z | y
  y | ka

By:	Rewrite (HigherC (LemmaC Thm* a,b:. ab = ba)) 0

1

y | ak

1 step

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