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
11. (a1) ~ (bc)
  False

1

11. (a1) ~ (ac)   False

4 steps

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