diff --git a/src/extra/DeBruijn.lagda b/src/extra/DeBruijn.lagda
index 66b71256..92d4432b 100644
--- a/src/extra/DeBruijn.lagda
+++ b/src/extra/DeBruijn.lagda
@@ -9,7 +9,7 @@ module DeBruijn where
 \begin{code}
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
-open Eq.≡-Reasoning
+-- open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
@@ -34,8 +34,8 @@ data Env : Set where
   _,_ : Env → Type → Env
 
 data Var : Env → Type → Set where
-  zero : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A
-  suc : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B
+  Z : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A
+  S : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B
 
 data Exp : Env → Type → Set where
   var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A
@@ -58,10 +58,10 @@ Church : Type
 Church = (o ⇒ o) ⇒ o ⇒ o
 
 plus : Exp ε (Church ⇒ Church ⇒ Church)
-plus =  (abs (abs (abs (abs (app (app (var (suc (suc (suc zero)))) (var (suc zero))) (app (app (var (suc (suc zero))) (var (suc zero))) (var zero)))))))
+plus =  (abs (abs (abs (abs (app (app (var (S (S (S Z)))) (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z)))))))
 
 one : Exp ε Church
-one =  (abs (abs (app (var (suc zero)) (var zero))))
+one =  (abs (abs (app (var (S Z)) (var Z))))
 
 two : Exp ε Church
 two = (app (app plus one) one)
@@ -75,55 +75,175 @@ four = (app (app plus two) two)
 
 \begin{code}
 lookup : ∀ {Γ : Env} {A : Type} → Var Γ A → env Γ → type A
-lookup zero ⟨ ρ , v ⟩ = v
-lookup (suc n) ⟨ ρ , v ⟩ = lookup n ρ
+lookup Z ⟨ ρ , v ⟩ = v
+lookup (S n) ⟨ ρ , v ⟩ = lookup n ρ
 
 eval : ∀ {Γ : Env} {A : Type} → Exp Γ A → env Γ → type A
 eval (var n) ρ  =  lookup n ρ
 eval (abs N) ρ  =  λ{ v → eval N ⟨ ρ , v ⟩ }
 eval (app L M) ρ  =  eval L ρ (eval M ρ)
 
-ex : eval four tt suc 0 ≡ 4
+ex : eval four tt suc zero ≡ 4
 ex = refl
 \end{code}
 
-# Operational semantics
+# Operational semantics - with substitution a la Darais (31 lines)
 
-## Substitution
+## Remove variable from environment (4 lines)
 
 \begin{code}
-extr : ∀ {Γ Δ : Env} {B : Type} → (∀ {A : Type} → Var Γ A → Var Δ A) → Var Δ B → (∀ {A : Type} → Var (Γ , B) A → Var Δ A)
-extr ρ v zero     =  v
-extr ρ v (suc k)  =  ρ k
-
-ren : ∀ {Γ Δ : Env} → (∀ {A : Type} → Var Γ A → Var Δ A) → (∀ {A : Type} → Exp Γ A → Exp Δ A)
-ren ρ (var n)    =  var (ρ n)
-ren ρ (app L M)  =  app (ren ρ L) (ren ρ M)
-ren ρ (abs N)    =  abs (ren (extr (suc ∘ ρ) zero) N)
+infix 4 _⊝_
+_⊝_ : ∀ {A : Type} (Γ : Env) → Var Γ A → Env
+(Γ , B) ⊝ Z = Γ
+(Γ , B) ⊝ S k = (Γ ⊝ k) , B
 \end{code}
 
+## Rebuild environment (6 lines)
+
+\begin{code}
+shunt : ∀ (Γ Δ : Env) → Env
+shunt Γ ε = Γ
+shunt Γ (Δ , A) = shunt (Γ , A) Δ
+
+weaken : ∀ (Γ Δ : Env) {A : Type} (k : Var Γ A) → Var (shunt Γ Δ) A
+weaken Γ ε k = k
+weaken Γ (Δ , A) k = weaken (Γ , A) Δ (S k)
+\end{code}
+
+## Lift term to a larger environment (8 lines)
+
+\begin{code}
+liftvar : ∀ {Γ : Env} {A B : Type} (j : Var Γ B) (k : Var (Γ ⊝ j) A) → Var Γ A
+liftvar Z k = S k
+liftvar (S j) Z = Z
+liftvar (S j) (S k) = S (liftvar j k)
+
+lift : ∀ {Γ : Env} {A B : Type} (j : Var Γ B) (M : Exp (Γ ⊝ j) A) → Exp Γ A
+lift j (var k)    =  var (liftvar j k)
+lift j (abs N)    =  abs (lift (S j) N)
+lift j (app L M)  =  app (lift j L) (lift j M)
+\end{code}
+
+## Substitution (13 lines)
+
+\begin{code}
+substvar : ∀ (Γ Δ : Env) {A B : Type} (j : Var Γ B) (k : Var Γ A) (P : Exp (shunt (Γ ⊝ k) Δ) A) → Exp (shunt (Γ ⊝ k) Δ) B
+substvar Γ Δ Z Z P = P
+substvar (Γ , A) Δ Z (S k) P = var (weaken ((Γ ⊝ k) , A) Δ Z)
+substvar (Γ , A) Δ (S j) Z P = var (weaken Γ Δ j)
+substvar (Γ , A) Δ (S j) (S k) P = substvar Γ (Δ , A) j k P
+
+subst : ∀ {Γ : Env} {A B : Type} (N : Exp Γ B) (k : Var Γ A) (M : Exp (Γ ⊝ k) A) → Exp (Γ ⊝ k) B
+subst {Γ} (var j) k P = substvar Γ ε j k P
+subst (abs N) k P =  abs (subst N (S k) (lift Z P))
+subst (app L M) k P =  app (subst L k P) (subst M k P)
+\end{code}
+
+# Operational semantics - with simultaneous substitution, a la McBride (18 lines)
+
+## Renaming (7 lines)
+
+\begin{code}
+extend : ∀ {Γ Δ : Env} {B : Type} → (∀ {A : Type} → Var Γ A → Var Δ A) → Var Δ B → (∀ {A : Type} → Var (Γ , B) A → Var Δ A)
+extend ρ j Z      =  j
+extend ρ j (S k)  =  ρ k
+
+rename : ∀ {Γ Δ : Env} → (∀ {A : Type} → Var Γ A → Var Δ A) → (∀ {A : Type} → Exp Γ A → Exp Δ A)
+rename ρ (var n)    =  var (ρ n)
+rename ρ (abs N)    =  abs (rename (extend (S ∘ ρ) Z) N)
+rename ρ (app L M)  =  app (rename ρ L) (rename ρ M)
+\end{code}
+
+## Substitution (9 lines)
+
 \begin{code}
 ext :  ∀ {Γ Δ : Env} {B : Type} → (∀ {A : Type} → Var Γ A → Exp Δ A) → Exp Δ B → (∀ {A : Type} → Var (Γ , B) A → Exp Δ A)
-ext ρ v zero     =  v
-ext ρ v (suc k)  =  ρ k
-
-emp : ∀ {Γ : Env} → (∀ {A : Type} → Var Γ A → Exp Γ A)
-emp k = var k
+ext ρ j Z      =  j
+ext ρ j (S k)  =  ρ k
 
 sub : ∀ {Γ Δ : Env} → (∀ {A : Type} → Var Γ A → Exp Δ A) → (∀ {A : Type} → Exp Γ A → Exp Δ A)
 sub ρ (var n)    =  ρ n
 sub ρ (app L M)  =  app (sub ρ L) (sub ρ M)
-sub ρ (abs N)    =  abs (sub (ext (ren suc ∘ ρ) (var zero)) N)
+sub ρ (abs N)    =  abs (sub (ext (rename S ∘ ρ) (var Z)) N)
 
-subst : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ A → Exp Γ B
-subst N M =  sub (ext emp M) N 
+substitute : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ A → Exp Γ B
+substitute N M =  sub (ext var M) N 
+\end{code}
+
+## Value
+
+\begin{code}
+data Val : {Γ : Env} {A : Type} → Exp Γ A → Set where
+  Fun : ∀ {Γ : Env} {A B : Type} {N : Exp (Γ , A) B} →
+    Val (abs N)
 \end{code}
 
 ## Reduction step
 
 \begin{code}
-data Val : {Γ : Env} {A : Type} → Exp Γ A → Set where
-
-data Step : {Γ : Env} {A : Type} → Exp Γ A → Exp Γ A → Set where
-  beta : ∀ {Γ : Env} {A B : Type} {N : Exp (Γ , A) B} {M : Exp Γ A} → Step (app (abs N) M) (subst N M) 
+data _⟶_ : {Γ : Env} {A : Type} → Exp Γ A → Exp Γ A → Set where
+  ξ₁ : ∀ {Γ : Env} {A B : Type} {L : Exp Γ (A ⇒ B)} {L′ : Exp Γ (A ⇒ B)} {M : Exp Γ A} →
+     L ⟶ L′ →
+     app L M ⟶ app L′ M
+  ξ₂ : ∀ {Γ : Env} {A B : Type} {L : Exp Γ (A ⇒ B)} {M : Exp Γ A} {M′ : Exp Γ A} →
+     Val L →
+     M ⟶ M′ →
+     app L M ⟶ app L M′
+  β : ∀ {Γ : Env} {A B : Type} {N : Exp (Γ , A) B} {M : Exp Γ A} → 
+    Val M → 
+    app (abs N) M ⟶ substitute N M
 \end{code}
+
+## Reflexive and transitive closure
+
+\begin{code}
+data _⟶*_ : {Γ : Env} {A : Type} → Exp Γ A → Exp Γ A → Set where
+  reflexive : ∀ {Γ : Env} {A : Type} {M : Exp Γ A} →
+    M ⟶* M
+  inclusion : ∀ {Γ : Env} {A : Type} {L M : Exp Γ A} →
+    L ⟶ M →
+    L ⟶* M
+  transitive : ∀ {Γ : Env} {A : Type} {L M N : Exp Γ A} →
+    L ⟶* M →
+    M ⟶* N →
+    L ⟶* N
+\end{code}
+
+## Displaying reduction sequences
+
+\begin{code}
+infix 1 begin_
+infixr 2 _⟶⟨_⟩_
+infix 3 _∎
+
+begin_ : {Γ : Env} {A : Type} {M N : Exp Γ A} → (M ⟶* N) → (M ⟶* N)
+begin steps = steps
+
+_⟶⟨_⟩_ : {Γ : Env} {A : Type} (L : Exp Γ A) {M N : Exp Γ A} → (L ⟶ M) → (M ⟶* N) → (L ⟶* N)
+L ⟶⟨ L⟶M ⟩ M⟶*N = transitive (inclusion L⟶M) M⟶*N
+
+_∎ : {Γ : Env} {A : Type} (M : Exp Γ A) → M ⟶* M
+M ∎ = reflexive
+\end{code}
+
+## Example reduction sequence
+
+\begin{code}
+ex₁ : (app (abs (var Z)) (abs (var Z))) ⟶* (abs (var Z))
+ex₁ =
+  begin
+    (app (abs (var Z)) (abs (var Z)))
+  ⟶⟨ β ⟩
+    (abs (var Z))
+  ∎
+\end{code}
+
+ex₁ : (app (app plus one) one) ⟶ (abs (abs (app (var (S Z)) (app (var (S Z)) (var Z)))))
+ex₁ =
+  begin
+    (app (app plus one) one)
+  ⟶⟨ ξ_1 β ⟩
+    (app (abs (abs (abs (app (app one) (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z))))) one)
+  ⟶⟨ β ⟩
+    (abs (abs (app (app one) (var (S Z))) (app (app one (var (S Z))) (var Z))))
+  ⟶⟨ ⟩