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

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 2 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. j : T
9.

k:T. r(k,j)

(

n:S. f(n) = k

P(n))
10. n : S
11. f(n) = j

P(n)

By:

p.
let y

get_var_arg `n` p ,
let yy

get_var_arg `nn` p ,
let S

get_term_arg `S` p ,
let r

get_term_arg `f` p ,
let j

var_of_hyp -4 p ,
let k,(),T1

dest_all (h -3 p) ,
let k_lt_j,()

dest_implies T1 ,
let ryy_lt_ry
let

subst [k,(mk_apply_term r (mvt yy));j,(mk_apply_term r (mvt y))] k_lt_j ,
let P_yy

subst [y,(mvt yy)] (concl p) in
Assert (mk_all_term yy S (mk_implies_term ryy_lt_ry P_yy)) p

Generated subgoals:

1   nn:S. r(f(nn),f(n))  P(nn)
10 steps

2 12. nn:S. r(f(nn),f(n))  P(nn)
  P(n)
2 steps

About:

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

1	nn:S. r(f(nn),f(n)) P(nn)	10 steps
2	12. nn:S. r(f(nn),f(n)) P(nn) P(n)	2 steps