support for logic defs + decompile translations bool <-> prop
This patch extends the BDD-infer engine:
- logic functions in annotations are supported when they have a definition. In that case, the definition is simply inlined for inference
- terms where some transparent translation between bool and prop have been added are now supported. For example, a formula like
andb b (x=y)
is properly normalized intob /\ (x=y)
and not the horrible(andb b (if x=y the True else False)) = True