> That is, it usually makes your life easier if you don't use "with" > in definitions that you later will want to prove something about. Reminds me of the the Coq situation where it's recommended not to use tactics for definitions. Stefan