1. a : 
2. 0<a
3. b,c:. (a-1)b = c  (((a-1)b) ~ c)
4. b : 
5. c : 
6. ab = c
  (ab) ~ (((a-1)b)+b)

By:	BackThru:  Thm*  a,b:, B:({a..b}Type). Thm*  a<b  ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1)))

None

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