##]
nqed.
+nlemma decidable_bexpr : ∀x.(x = true) ∨ (x = false).
+ #x; ncases x;
+ ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
+ ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+ ##]
+nqed.
+
nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
#b1; #b2;
ncases b1;
##]
nqed.
+nlemma eqfalse_to_neqtrue : ∀x.x = false → x ≠ true.
+ #x; nelim x;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##]
+nqed.
+
+nlemma eqtrue_to_neqfalse : ∀x.x = true → x ≠ false.
+ #x; nelim x;
+ ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##| ##2: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma neqfalse_to_eqtrue : ∀x.x ≠ false → x = true.
+ #x; nelim x;
+ ##[ ##1: #H; napply refl_eq
+ ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
+ ##]
+nqed.
+
+nlemma neqtrue_to_eqfalse : ∀x.x ≠ true → x = false.
+ #x; nelim x;
+ ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
+ ##| ##2: #H; napply refl_eq
+ ##]
+nqed.
+
nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
#b1; #b2;
ncases b1;