Nuprl - Proof: trivial factorization comp1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trivial factorization comp1

x,y:

. x = y

trivial_factorization(x)(y) = 1

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 = 1
1 step

About:

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