IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one one corr rel vs invfuns111 1. A : Type
2. B : Type
3. R : ABProp
4. x:A. !y:B. R(x;y)
5. y:B. !x:A. R(x;y)
f:(AB), g:(BA).
InvFuns(A;B;f;g) & (x:A, y:B. R(x;y) y = f(x) & x = g(y))
By:
FwdThru:
Thm* (x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x)))
on [ Hyp:4 ]
THEN
SimilarTo: Hyp:-1
THEN
FwdThru:
Thm* (x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x)))
on [ Hyp:5 ]
THEN
CBV-1: g THEN
SimilarTo: Hyp:-1