Nuprl - Proof: inv image ind tp 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv image ind tp 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. n : S

P(n)

By:	PushArgs [`f`,(term_to_arg f) ;`T`,(term_to_arg T) ;`n`,(var_to_arg `n') ;`nn`,(var_to_arg `nn') ;`S`,(term_to_arg S) ;`i`,(int_to_arg 8) ;`RangeIndTac`,(tactic_to_arg (WFndHypInd 5 -1))]

Generated subgoal:

1 P(n)
28 steps

About:

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