diff options
-rw-r--r-- | unit-tests/Tests.v | 4 |
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. |