diff --git a/src/Data/Can/Properties.agda b/src/Data/Can/Properties.agda
index 488f83c..160b163 100644
--- a/src/Data/Can/Properties.agda
+++ b/src/Data/Can/Properties.agda
@@ -81,13 +81,13 @@ module _ {la lb} {A : Set la} {B : Set lb} where
              (deca a1 a2 *-dec decb b1 b2)
   ≡-dec deca decb non (one a) = no \ ()
   ≡-dec deca decb non (eno b) = no \ ()
-  ≡-dec deca decb non (two a b) = no \ ()
-  ≡-dec deca decb (one a) non = no \ ()
-  ≡-dec deca decb (one a) (eno b) = no \ ()
-  ≡-dec deca decb (one a1) (two a2 b2) = no \ ()
+  ≡-dec deca decb non (two a b) = no \ ()
+  ≡-dec deca decb (one a) non = no \ ()
+  ≡-dec deca decb (one a) (eno b) = no \ ()
+  ≡-dec deca decb (one a1) (two a2 b2) = no \ ()
   ≡-dec deca decb (eno b) non = no \ ()
   ≡-dec deca decb (eno b) (one a) = no \ ()
-  ≡-dec deca decb (eno b1) (two a b2) = no \ ()
-  ≡-dec deca decb (two a b) non = no \ ()
-  ≡-dec deca decb (two a1 b) (one a2) = no \ ()
-  ≡-dec deca decb (two a b1) (eno b2) = no \ ()
+  ≡-dec deca decb (eno b1) (two a b2) = no \ ()
+  ≡-dec deca decb (two a b) non = no \ ()
+  ≡-dec deca decb (two a1 b) (one a2) = no \ ()
+  ≡-dec deca decb (two a b1) (eno b2) = no \ ()