PROP_ATOM_CONV : conv -> conv
# PROP_ATOM_CONV(ONCE_DEPTH_CONV SYM_CONV) `(!x. x = y ==> x = z) <=> (y = z <=> 1 + z = z + 1)`;; val it : thm = |- ((!x. x = y ==> x = z) <=> y = z <=> 1 + z = z + 1) <=> (!x. y = x ==> z = x) <=> z = y <=> z + 1 = 1 + z