FOL.lp

// (multi-sorted) First-order logic

require open Stdlib.Set Stdlib.Prop;

// Universal quantification

constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall

rule π (∀ $f) ↪ Π x, π ($f x);

// Existential quantification

constant symbol ∃ [a] : (τ a → Prop) → Prop; notation ∃ quantifier; // ?? or \exists

constant symbol ∃ᵢ [a] p (x:τ a) : π (p x) → π (∃ p);
symbol ∃ₑ [a] p : π (∃ p) → Π q, (Π x:τ a, π (p x) → π q) → π q;

rule ∃ₑ _ (∃ᵢ _ $x $px) _ $f ↪ $f $x $px;