IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub inj lop typing1123 1. a : 2. b : 3. f : ab 4. Inj(a; b; f)
5. (a-1)
6. a2 : (a-1)
f(a2) {x:b| x = f(a-1) }
By:
{Similarly } Analyze THEN Analyze THEN FwdThru: Hyp:4 on [ f(a2) = f(a-1) b ]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
f(a2) 
{x:
x = f(a-1) }
