B:Type, e:(BB).
  IsEqFun(B;e)
  
  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a)

1

1. B : Type 2. e : BB 3. IsEqFun(B;e) 4. a :  5. f : a onto B   (y.least x:. (f(x)) e y)  B inj a

13 steps

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