eta-expand forall argument (#49)

Author: fblanqui

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 }

FOL.lp

@@ -10,7 +10,7 @@ builtin "all" ≔ ∀;
 
 notation ∀ quantifier;
 
-rule π (∀ $f) ↪ Π x, π ($f x);
+rule π (`∀ x, $f.[x]) ↪ Π x, π $f.[x];
 
 // Existential quantification