-lemma commutative_orb: commutative … orb.
-* * // qed.
-
-lemma orb_true_dx: ∀b. (b ∨ Ⓣ) = Ⓣ.
-* // qed.
-
-lemma orb_true_sn: ∀b. (Ⓣ ∨ b) = Ⓣ.
-// qed.
-
-lemma commutative_andb: commutative … andb.
-* * // qed.
-
-lemma andb_false_dx: ∀b. (b ∧ Ⓕ) = Ⓕ.
-* // qed.
-
-lemma andb_false_sn: ∀b. (Ⓕ ∧ b) = Ⓕ.
-// qed.
-
-lemma eq_bool_dec: ∀b1,b2:bool. Decidable (b1 = b2).