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

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

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. n : S
9.

x:T, n:S. f(n) = x

P(n)

By:	p. let y get_var_arg `n` p , let r get_term_arg `f` p in ((DTerm (mk_apply_term r (mvt y)) -1) THEN (DTerm (mvt y) -1 THENA Declaration) (THEN ((Analyze -1) (THEN (Hypothesis) p

Generated subgoals:

1 f(n) T
1 step

2 f(n) = f(n)
1 step

About:

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