Better automation in sets using workaround for 3410
Improve proof automation in sets.v