diff options
| -rw-r--r-- | examples/Example.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/examples/Example.v b/examples/Example.v index b83e619..5c740d6 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -62,10 +62,7 @@ Proof. zchaff. Qed. -Goal forall i j k, - let a := (i == j)%int in - let b := (j == k)%int in - let c := (k == i)%int in +Goal forall a b c, (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. Proof. zchaff. |