diff --git a/Prop.lp b/Prop.lp
index 32f0f22..bce4400 100644
--- a/Prop.lp
+++ b/Prop.lp
@@ -14,12 +14,16 @@ builtin "Prf" ≔ π;
 
 constant symbol ⊤ : Prop; // \top
 
+builtin "top" ≔ ⊤;
+
 constant symbol ⊤ᵢ : π ⊤;
 
 // false
 
 constant symbol ⊥ : Prop; // \bot
 
+builtin "bot" ≔ ⊤;
+
 constant symbol ⊥ₑ [p] : π ⊥ → π p;
 
 // implication
@@ -28,6 +32,8 @@ constant symbol ⇒ : Prop → Prop → Prop; // =>
 
 notation ⇒ infix right 5;
 
+builtin "imp" ≔ ⇒;
+
 rule π ($p ⇒ $q) ↪ π $p → π $q;
 
 symbol fold_⇒ [p q] : π (p ⇒ q) → π p → π q ≔
@@ -41,12 +47,16 @@ symbol ¬ p ≔ p ⇒ ⊥; // ~~ or \neg
 
 notation ¬ prefix 35;
 
+builtin "not" ≔ ¬;
+
 // conjunction
 
 constant symbol ∧ : Prop → Prop → Prop; // /\ or \wedge
 
 notation ∧ infix right 7;
 
+builtin "and" ≔ ∧;
+
 constant symbol ∧ᵢ [p q] : π p → π q → π (p ∧ q);
 symbol ∧ₑ₁ [p q] : π (p ∧ q) → π p;
 symbol ∧ₑ₂ [p q] : π (p ∧ q) → π q;
@@ -57,6 +67,8 @@ constant symbol ∨ : Prop → Prop → Prop; // \/ or \vee
 
 notation ∨ infix right 6;
 
+builtin "or" ≔ ∨;
+
 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;
@@ -67,6 +79,8 @@ symbol ⇔ p q ≔ (p ⇒ q) ∧ (q ⇒ p); // \Leftrightarrow
 
 notation ⇔ infix right 5;
 
+builtin "eqv" ≔ ⇔;
+
 opaque symbol ⇔_refl [p] : π (p ⇔ p) ≔
 begin
   assume p; apply ∧ᵢ { assume h; apply h } { assume h; apply h }