fact: Definition make_is_boolean {X : hSet} (L : bounded_lattice X) : is_distributive L -> complemented_structure L -> is_boolean L.
imports: UniMath.Foundations.Preamble UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.OrderTheory.Lattice.Complement UniMath.OrderTheory.Lattice.Distributive UniMath.OrderTheory.Lattice.Heyting