1. a : 
2. a1:. a1<a  (b:. (a1 inj b) ~ (b!a1))
3. b : 
4. ab
5. a = 0
  (a inj b) ~ (b(b-1)!(a-1))

By:	Rewrite by Thm*  a,b:. (a inj b) ~ (b((a-1) inj (b-1)))

1

(b((a-1) inj (b-1))) ~ (b(b-1)!(a-1))

3 steps

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