diff --git a/algebra/csum.v b/algebra/csum.v
index d8a4d66ad172423785dd71629045f3323e0c93e2..21102960721c29b4ffbaad4a5a70fe42fa09b2c5 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -15,6 +15,11 @@ Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
 Arguments CsumBot {_ _}.
 
+Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
+  match x with Cinl a => Some a | _ => None end.
+Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
+  match x with Cinr b => Some b | _ => None end.
+
 Section cofe.
 Context {A B : cofeT}.
 Implicit Types a : A.