Nuprl - Proof: negnegelim imp notfin imp unb inf 1 2 1 1 1 1 1 2 1

(22steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: negnegelim imp notfin imp unb inf 1 2 1 1 1 1 1 2 1

1.

P:Prop.

P

P
2. A : Type
3.

(

n:

. A ~

n)
4. k :

5. 0<k
6. f :

(k-1)

A
7. Inj(

(k-1); A; f) [not for witness]
8. b : A
9.

(

i:

(k-1). f(i)

b)

a:

(k-1). f(a) = b

By:	BackThru: Hyp:1 THEN SimilarTo Hyp:9

Generated subgoal:

1 9. (a:(k-1). f(a) = b)
i:(k-1). f(i) b
1 step

About:

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

(22steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc