Ident theory solver

[volodeyka]

In this PR I tried to introduce the lia analogue for arbitrary identType. I have no idea how to call it, so for now its name is hal :)) hal just tries to make some preprocessing to transform some propositions on idents to correspondent propositions on nat's. After that hal calls lia If you want to make just preprocessing where it is possible, you can use encodify tactic

[volodeyka]

Also, the name hal does not tell anything to me :) Perhaps, ident_solver or ident_simpl ?

Yes, we decently should rename it :) But I think may it would be better to use some abbreviation, as it was done in the following examples:

• lia is a decision procedure for linear integer arithmetic;
• nia is an incomplete proof procedure for integer non-linear arithmetic;
• lra is a decision procedure for linear (real or rational) arithmetic;
• nra is an incomplete proof procedure for non-linear (real or rational) arithmetic;

Maybe lio : linear ident order or something like that?