IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub inj lop typing11221 1. a :
2. b :
3. f : ab 4. Inj(a; b; f)
5. a1 : (a-1)
6. (a-1)
7. f(a1) = f(a-1)
False
By:
FwdThru: Hyp:4 on [ f(a1) = f(a-1) b ]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html