aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests
diff options
context:
space:
mode:
Diffstat (limited to 'unit-tests')
-rw-r--r--unit-tests/Tests_verit.v6
1 files changed, 6 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index e99e484..ccc2714 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -527,6 +527,12 @@ Proof.
Qed.
+Goal forall x y, Bool.eqb (negb (xorb x y)) ((x && y) || ((negb x) && (negb y))).
+Proof.
+ verit.
+Qed.
+
+
Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)).
Proof.
verit.