p:. 
  prime(p)
  
  (a,b:, e:({a..b}).
  (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))

By:	Guarding (b:<type>. <prop>) Auto

1

1. p :  2. prime(p) 3. a :    b:, e:({a..b}).   a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i))

14 steps

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