diff --git a/README.org b/README.org
index 14d3f03..e5d5aee 100644
--- a/README.org
+++ b/README.org
@@ -119,20 +119,20 @@ Here is an example file defining Leibniz equality and proving that it is reflexi
   
   -- Defining Leibniz equality
   -- Note that we can leave the ascription off
-  eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+  def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
 
   -- Equality is reflexive, which is easy to prove
   -- Here we give an ascription so that when `perga` reports the type,
   -- it references `eq` rather than inferring the type.
-  eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+  def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
 
   -- Equality is symmetric. This one's a little harder to prove.
-  eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x :=
+  def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x :=
       fun (P : A -> *) (Hy : P y) =>
           Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
 
   -- Equality is transitive.
-  eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z :=
+  def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z :=
       fun (P : A -> *) (Hx : P x) => Hyz P (Hxy P Hx);
 #+end_src
 Running =perga equality.pg= yields the following output.