Definition bounded_prebilattice_to_prebilattice X (b : bounded_prebilattice X) : prebilattice X := make_prebilattice (pr1 b) (pr2 b) .
Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.