From 0c4d828ee2a41b17fe5862db6af79cd3c2c8acb0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 16 Oct 2025 15:21:18 +0200
Subject: [PATCH] eta-expand forall argument

---
 Classic.lp | 2 +-
 FOL.lp     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Classic.lp b/Classic.lp
index 0179e1d..2c444c3 100644
--- a/Classic.lp
+++ b/Classic.lp
@@ -18,7 +18,7 @@ assume p q pq; apply ∨ₑ (em p)
 { assume np; refine ∨ᵢ₁ np }
 end;
 
-opaque symbol ∃¬ᵢ a p : π (¬ (∀ p)) → π (`∃ x : τ a, ¬ (p x)) ≔
+opaque symbol ∃¬ᵢ a p : π (¬ (`∀ x, p x)) → π (`∃ x : τ a, ¬ (p x)) ≔
 begin
 assume a p not_all_p; apply ∨ₑ (em (`∃ x, ¬ (p x)))
 { assume h; apply h }
diff --git a/FOL.lp b/FOL.lp
index c99231d..71b040a 100644
--- a/FOL.lp
+++ b/FOL.lp
@@ -10,7 +10,7 @@ builtin "all" ≔ ∀;
 
 notation ∀ quantifier;
 
-rule π (∀ $f) ↪ Π x, π ($f x);
+rule π (`∀ x, $f.[x]) ↪ Π x, π $f.[x];
 
 // Existential quantification