1. a : 
2. b : 
3. j : b
4. f : (a-1){x:b| x = j }
5. Inj((a-1); {x:b| x = j }; f)
  (i.if i=a-1 j else f(i) fi)  a inj b

By:	(i.if i=a-1 j else f(i) fi)  ab  Asserted THEN Analyze

1	(i.if i=a-1 j else f(i) fi)  ab	2 steps
2	6. (i.if i=a-1 j else f(i) fi)  ab   Inj(a; b; i.if i=a-1 j else f(i) fi)	8 steps

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