(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 3

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:Sr(f(k),f(j))  P(k))  P(j)
8. j : T
  (k:Tr(k,j (n:Sf(n) = k  P(n)))  Prop


By: AddHiddenLabel `wf`


Generated subgoal:

1   (k:Tr(k,j (n:Sf(n) = k  P(n)))  Prop
1 step

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

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