Added an induction axiom for concrete predicates to prove them. So a lot
of lemmas from lists theory also proved.