diff --git a/theories/common.elpi b/theories/common.elpi
index 5f28353..237ffd9 100644
--- a/theories/common.elpi
+++ b/theories/common.elpi
@@ -7,6 +7,7 @@ list-constant T [X|XS] {{ @cons lp:T lp:X lp:XS' }} :- list-constant T XS XS'.
 
 pred mem o:list term, o:term, o:int.
 mem [X|_] X 0 :- !.
+mem [Y|_] X 0 :- Y = app [H|_], X = app [H|_], coq.unify-eq X Y ok, !.
 mem [_|XS] X M :- !, mem XS X N, M is N + 1.
 
 % [eucldiv N D M R] N = D * M + R