diff --git a/coq/DemoSyntaxReduction.v b/coq/DemoSyntaxReduction.v
index 4721df42e3f8c7a6c5ad4f1e94a775b3fdc7bf55..7436a73a7c753804aac2817ba9e1db8bb289bf40 100644
--- a/coq/DemoSyntaxReduction.v
+++ b/coq/DemoSyntaxReduction.v
@@ -31,6 +31,8 @@ Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (* A demo of the tactics [autosubst] and [asimpl]. *)
 
+(* (λx. x y)[σ] = (λx. x y[⇑σ]) *)
+
 Goal
   forall sigma,
   (Lam (App (Var 0) (Var 1))).[sigma] =
@@ -106,6 +108,7 @@ Inductive red : term -> term -> Prop :=
     forall t1 t2 u,
     t1.[t2/] = u ->
     red (App (Lam t1) t2) u
+    (* (λx.t1) t2 → [t2/x]t1 *)
 
 (* Reduction in the left-hand side of an application. *)
 | RedAppL:
@@ -144,9 +147,11 @@ Local Hint Extern 1 (_ = _) => autosubst : autosubst.
 
 Definition Delta :=
   Lam (App (Var 0) (Var 0)).
+  (* Δ := λx.(x x) *)
 
 Definition Omega :=
   App Delta Delta.
+  (* Ω := (Δ Δ) *)
 
 Goal
   red Omega Omega.