1. a : 
2. (a ~ 1)
3. b:. b | a  (b ~ 1)  (b ~ a)
4. b : 
5. c : 
6. (b ~ 1)
7. (c ~ 1)
8. a = bc
9. b ~ a
10. c ~ a
  False

By:	Assert ((a1) ~ (bc)) THENA StrengthenRel

1

11. (a1) ~ (bc)   False

5 steps

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