Nuprl - Proof: inv image ind tp 1 1 1 1 1 1

(32steps total) PrintForm Definitions well fnd Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv image ind tp 1 1 1 1 1 1

1. T : Type
2. r : T

Prop
3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S

Prop
7.

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j)
8. x : T

n:S. f(n) = x

P(n)

By:	p.get_tactic_arg `RangeIndTac` p p

Generated subgoals:

1   (x.n:S. f(n) = x  P(n))  TProp
2 steps

2 8. j : T
9. k:T. r(k,j)  (n:S. f(n) = k  P(n))
  n:S. f(n) = j  P(n)
16 steps

3 8. j : T
  (k:T. r(k,j)  (n:S. f(n) = k  P(n)))  Prop
2 steps

4   T  Type
1 step

About:

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

(32steps total) PrintForm Definitions well fnd Sections StandardLIB Doc

1	(x.n:S. f(n) = x P(n)) TProp	2 steps
2	8. j : T 9. k:T. r(k,j) (n:S. f(n) = k P(n)) n:S. f(n) = j P(n)	16 steps
3	8. j : T (k:T. r(k,j) (n:S. f(n) = k P(n))) Prop	2 steps
4	T Type	1 step