Lemma is_interlaced_FOUR : is_interlaced FOUR . Proof. exact (prod_prebilattices_are_interlaced FOUR) . Defined.
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.