Nuprl - Proof: fun with inv is bij 1 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun with inv is bij 1 1 2 1 1

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

B
4. g : B

A
5. g o f = Id
6. b : B
7. (f o g)(b) = Id(b)

f(g(b)) = b

By:	RW (SemiNormC [`compose`;`tidentity`;`identity`]) 7

Generated subgoal:

1 7. f(g(b)) = b
f(g(b)) = b
Trivial

About:

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