test-suite/success/btauto.v


1
2
3
4
5
6
7
8
9

Require Import Btauto.

Open Scope bool_scope.

Lemma test_orb a b : (if a || b then negb (negb b && negb a) else negb a && negb b) = true.
Proof. btauto. Qed.

Lemma test_xorb a : xorb a a = false.
Proof. btauto. Qed.