proposition: Lemma boolset_lattice_is_distributive : is_distributive boolset_lattice.
proof: Proof. intros b1 b2 b3; induction b1, b2, b3; reflexivity. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Bool UniMath.Algebra.BinaryOperations UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.OrderTheory.Lattice.Distributive UniMath.OrderTheory.Lattice.Complement UniMath.OrderTheory.Lattice.Boolean