(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 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:Sr(f(k),f(j))  P(k))  P(j)
  (x.n:Sf(n) = x  P(n))  TProp


By: AddHiddenLabel `wf`


Generated subgoal:

1   (x.n:Sf(n) = x  P(n))  TProp
1 step

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

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