At: nsub surj least preimage total gen

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

1

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

7 steps

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