(*#* This file centralizes the lemmas about [Z], classifying them
according to the way they can be used in automatic search *)
(*#* This file centralizes the lemmas about [Z], classifying them
according to the way they can be used in automatic search *)