(2steps total) PrintForm Definitions FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trivial factorization comp2
  x,y:. x  y  trivial_factorization(x)(y) = 0  
By: Def of trivial_factorization(<term>) THEN Reduce Concl

Generated subgoal:

1 1. x : 
2. y : 
3. x  y
  if y=x 1 else 0 fi = 0  
1 step

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

(2steps total) PrintForm Definitions FTA Sections DiscrMathExt Doc