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

1

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

11 steps

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