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.
In Poi, since constants are defined as "function of something that returns the constant", e.g.
\true, it is possible to prove:while the following is also provable due to the function inequalities:
This means that function equality is inconsistent.
For now, reductions rules are added to override into the second case, while
(= true) <=> idbis an equivalence. This means that the inconsistency disappears when reductions are applied before equivalences.