aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--unit-tests/Tests.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/unit-tests/Tests.v b/unit-tests/Tests.v
index d011cdb..3b8d95a 100644
--- a/unit-tests/Tests.v
+++ b/unit-tests/Tests.v
@@ -65,6 +65,10 @@ Goal forall a, negb (a || negb a) = false.
zchaff.
Qed.
+Goal forall a, negb (negb (a || negb a)).
+ zchaff.
+Qed.
+
Goal forall a, (a && negb a) = false.
zchaff.
Qed.