Lemma andb_is_associative : ∏ b1 b2 b3 : bool, andb (andb b1 b2) b3 = andb b1 (andb b2 b3). Proof. intros; induction b1; induction b2; induction b3; reflexivity. Qed.
Require Import UniMath.Foundations.Init. Require Import UniMath.Foundations.Sets.