1. A : Type
2. A ~ 1
  !A

1

2. f : A1 3. g : 1A 4. InvFuns(A;1;f;g)   !A

3 steps

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