Handling inconsistency of function equality

[bvssvni]

In Poi, since constants are defined as "function of something that returns the constant", e.g. \true, it is possible to prove:

true = id
(= true)(id)
idb(id)
id(id)
id

while the following is also provable due to the function inequalities:

true = id
id = true
false

This means that function equality is inconsistent.

For now, reductions rules are added to override into the second case, while (= true) <=> idb is an equivalence.
This means that the inconsistency disappears when reductions are applied before equivalences.