IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite inj counter example1111 1. m : 2. f : m 3. Inj(m; ; f)
4. (x:m, y:x. f(x) = f(y))
5. a1 : m 6. a2 : m 7. f(a1) = f(a2)
8. a1<a2 x:m, y:x. f(x) = f(y)
By:
Witness: a2 THEN Witness: a1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Inj(
x:
