From 40fbf43ce5e7e56ad42c9958b58aea0f298d177f Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Wed, 22 Jan 2025 14:07:35 +0100
Subject: [PATCH] check heads before unifying

---
 theories/common.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/common.elpi b/theories/common.elpi
index 68e81e5..237ffd9 100644
--- 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