At: iter nat prod one iff factors one

  a,b:, e:({a..b}). ( i:{a..b}. e(i)) = 1  (i:{a..b}. e(i) = 1)

By:	Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i)) Asserted THEN Guarding (i:<type>. <prop>) Rewrite by Hyp:-1 THEN Thin Hyp:-1 THEN Analyze

1

1. a :    b:, e:({a..b}). ( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1)

13 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html