Nuprl - Proof: bij iff is 1 1 corr 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bij iff is 1 1 corr 1

1. A : Type
2. B : Type
3. f : A

Bij(A; B; f)

f is 1-1 corr

By:	Def of f is 1-1 corr

Generated subgoals:

1 4. Bij(A; B; f)
g:(BA). InvFuns(A;B;f;g)
1 step

2 4. g:(BA). InvFuns(A;B;f;g)
Bij(A; B; f)
2 steps

About:

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

1	4. Bij(A; B; f) g:(BA). InvFuns(A;B;f;g)	1 step
2	4. g:(BA). InvFuns(A;B;f;g) Bij(A; B; f)	2 steps