Nuprl - Proof: inv image ind tp

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv image ind tp

T:Type, r:(T

Prop), S:Type, f:(S

T).

WellFnd{i}(T;x,y.r(x,y))

WellFnd{i}(S;x,y.r(f(x),f(y)))

By:

UnivCD

Generated subgoal:

1 1. T : Type
2. r : TTProp
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
WellFnd{i}(S;x,y.r(f(x),f(y)))
31 steps

About:

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