1. a : 
2. (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))
3. b : 
4. c : 
5. a | bc
  a | b  a | c

1

2. (a ~ 1) 3. b:. b | a  (b ~ 1)  (b ~ a) 4. b :  5. c :  6. a | bc   a | b  a | c

10 steps

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