∀ {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z),
  BddDistLat.ofHom (BoolAlg.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (BddDistLat.ofHom (BoolAlg.Hom.hom f)) (BddDistLat.ofHom (BoolAlg.Hom.hom g))