check heads before unifying

math-comp · Jan 22, 2025 · 40fbf43 · 40fbf43
1 parent fc1b2ee
commit 40fbf43
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/common.elpi b/theories/common.elpi
@@ -7,7 +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 :- coq.unify-eq X Y ok, !.
+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