PLE diverges if boolean definitions are simplified

[facundominguez]

In order to reproduce, edit pleBoolC.fq as follows

diff --git a/tests/proof/pleBoolC.fq b/tests/proof/pleBoolC.fq
index 2efb3cfc..5161d4e9 100644
--- a/tests/proof/pleBoolC.fq
+++ b/tests/proof/pleBoolC.fq
@@ -27,8 +27,8 @@ constant tail: (func(1, [Vec @(0); Vec @(0)]))
 
 
 define mall(f:func(0,[int;bool]), xs:Vec int) : bool = {
-    if (isNil xs) then true 
-    else (mand (f (head xs)) (mall f (tail xs)))
+    (~(isNil xs)) => (mand (f (head xs)) (mall f (tail xs)))
 }
 
 define mand(x:bool, y:bool) : bool = { 

Then run

$ fixpoint --eliminate=some tests/proof/pleBoolC.fq

The expected outcome is that PLE succeeds, however the current behavior is that it never terminates.

This was first identified in #473 when implementing some simplifications on boolean conditions.