Hi Piotr, >Formalization takes long time because the data base has >holes I'm not sure that's the main problem. Generally in the little experiments that I do I can find the lemmas that I'm looking for... after a long time searching for them and trying to get the typing to work and everything. Freek