Lemma isaprop_is_interlaced {X : hSet} {b : prebilattice X} : isaprop (is_interlaced b). Proof. do 3 (try use (isapropdirprod)); use isaprop_interlacing. Defined.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Algebra.BinaryOperations.