diff options
Diffstat (limited to 'unit-tests')
-rw-r--r-- | unit-tests/Tests_verit.v | 6 |
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. |