Nuprl - Proof: finite inj counter example 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite inj counter example 1 1 1

1. m :

2. f :

Inj(

; f)
4.

(

m, y:

x. f(x) = f(y))
5. a1 :

m
6. a2 :

m
7. f(a1) = f(a2)

a1 = a2

By:	a1<a2 & a2<a1 Asserted THEN Analyze THEN Analyze4

Generated subgoals:

1 8. a1<a2
x:m, y:x. f(x) = f(y)
1 step

2 8. a2<a1
x:m, y:x. f(x) = f(y)
1 step

About:

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

1	8. a1<a2 x:m, y:x. f(x) = f(y)	1 step
2	8. a2<a1 x:m, y:x. f(x) = f(y)	1 step