Complete conversion of itab module

Well it's more straightforward than tactics module, so we do it first.
Revise tactics module until REFL_TAC function