(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. T : Type
2. r : TTProp
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : SProp
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. n : S
  P(n)
By: Analogy Tactic Directive: %S%

p.
let x  get_distinct_var `x' p ,
let n  get_var_arg `n` p ,
let S  get_term_arg `S` p ,
let T  get_term_arg `T` p ,
let f  get_term_arg `f` p in
Assert
(mk_all_term x T
((mk_all_term n S
(((mk_implies_term (mk_equal_term T (mk_apply_term f (mvt n)) (mvt x))
((((concl p))))
p

Generated subgoals:

1   x:T, n:S. f(n) = x  P(n)
24 steps
2 9. x:T, n:S. f(n) = x  P(n)
  P(n)
3 steps

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

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