diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda
index 7dc79d7..95a901f 100644
--- a/Lattice/Prod.agda
+++ b/Lattice/Prod.agda
@@ -94,6 +94,16 @@ isLattice = record
         )
     }
 
+
+module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
+    ≈-dec : IsDecidable _≈_
+    ≈-dec (a₁ , b₁) (a₂ , b₂)
+        with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
+    ...   | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
+    ...   | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
+    ...   | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
+
+
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
          (h₁ h₂ : ℕ)
          (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where