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