improve notations

Author: fblanqui

FOL.lp

@@ -16,5 +16,7 @@ constant symbol ∃ {a} : (τ a → Prop) → Prop;
 
 notation ∃ quantifier;
 
-constant symbol ex_intro {a} p (x:τ a) : π (p x) → π (∃ p);
-symbol ex_elim {a} p q : π (∃ p) → (Π x:τ a, π (p x) → π q) → π q;
+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;

Prop.lp

@@ -20,27 +20,27 @@ constant symbol top : π ⊤;
 
 constant symbol ⊥ : Prop;
 
-constant symbol false_elim p : π ⊥ → π p;
+constant symbol ⊥_elim p : π ⊥ → π p;
 
 // Conjunction
 
 constant symbol ∧ : Prop → Prop → Prop; // \wedge
 
 notation ∧ infix left 7;
 
-constant symbol conj_intro p q : π p → π q → π (p ∧ q);
-symbol conj_elim_left p q : π (p ∧ q) → π p;
-symbol conj_elim_right p q : π (p ∧ q) → π q;
+constant symbol ∧ᵢ p q : π p → π q → π (p ∧ q);
+symbol ∧ₑ₁ p q : π (p ∧ q) → π p;
+symbol ∧ₑ₂ p q : π (p ∧ q) → π q;
 
 // Disjunction
 
 constant symbol ∨ : Prop → Prop → Prop; // \vee
 
 notation ∨ infix left 6;
 
-constant symbol disj_intro_left p q : π p → π (p ∨ q);
-constant symbol disj_intro_right p q : π q → π (p ∨ q);
-symbol disj_elim p q r : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;
+constant symbol ∨ᵢ₁ p q : π p → π (p ∨ q);
+constant symbol ∨ᵢ₂ p q : π q → π (p ∨ q);
+symbol ∨ₑ p q r : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;
 
 // check that priorities are correctly set
 assert x y z ⊢ x ∨ y ∧ z ≡ x ∨ (y ∧ z);