IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
surjection type surjection A,B:Type, f:(A ontoB), a:. a ontoA (B Discrete) Surj(A; B; f)
By:
Auto
THEN
Rename-2: s THEN
Use:[a | A | B | f | s]
Inst: Thm*f:(B ontoC), g:(A ontoB). f o gA ontoC THEN
FwdThru:
Thm* (A Discrete) (e:(AA). x,y:A. (xey) x = y)
on [ B Discrete ]
THEN
Analyze-1