1. m : 
2. a : 
3. a' : 
4. b : 
5. b' : 
6. m | a-a'
7. m | b-b'
  m | ab-a'b'

By:	(Using [`c',b] (FwdThru Thm* a,b,c:. a | b  a | bc [6])) THEN (Using [`c',a'] (FwdThru Thm* a,b,c:. a | b  a | bc [7])) THEN (OnHyps [7;6] Thin)

1

6. m | (a-a')b 7. m | (b-b')a'   m | ab-a'b'

2 steps

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