1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
5. x<xx & x<xx
  split_factor1(g; x)(xx) = 0
  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))

By:	Auto THEN Def of split_factor1(<term>; <term>) THEN Reduce Concl THEN SplitOnConclITEs ...

None

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