diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 05bdbd34029621f632f2ffd9b2583101fbe3e188..84181b21c8b117e52771104d7a6ff12c6c978f0d 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -30,12 +30,12 @@ Implicit Types b : B.
 (* Cofe *)
 Inductive csum_equiv : Equiv (csum A B) :=
   | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
-  | Cinlr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
+  | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
   | CsumBot_equiv : CsumBot ≡ CsumBot.
 Existing Instance csum_equiv.
 Inductive csum_dist : Dist (csum A B) :=
   | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
-  | Cinlr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
+  | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
 Existing Instance csum_dist.