/Lattice/Bundle/
../
BoundedDistributive.agda