many changes:

many changes:
1) fixed many bugs and added support for implicit detection in
   cic -> declarative
2) added a tactic to find a proof rewriting n times with a given universe
   used instead of auto_paramodulation in the declarative language
   (here you know that 1 rewriting step with that lemma is enough)
3) added ESCAPE to sql queries using LIKE, to make sqlite and mysql compatible