I made a slight error in the definition of observational congruence; the corrected version is DEF: Two terms M and N are *observationally congruent* if for any closing context C[ ] with C[M], C[N] of integer type, Eval(C[M]) and Eval(C[N]) either both do not halt or one equals the numeral 0 iff the other equals 0. -Jon Riecke