Definition FOUR := make_bounded_prod_prebilattice boolset_bounded_lattice boolset_bounded_lattice .
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Prebilattice.Product. Require Import UniMath.OrderTheory.Prebilattice.Interlaced. Require Import UniMath.OrderTheory.Prebilattice.Distributive. Require Import UniMath.OrderTheory.Lattice.Examples.Bool. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Bool.