Here's my formal definition of substitution. Since I wasn't in class last week, I'm not sure what notational conventions are being used, so I'll define my grammar first.

```ebnf
n, m :: Nat
a, b, c :: Term ::= n | λ b | b a
r :: Nat -> Nat
```

I'm using simultaneous renamings r mapping from indices to indices. Lifting a renaming means weakening by 1, so the new mapping refers to the previous entry in the old mapping, and increments what it maps to, defined below.

```haskell
lift :: (Nat → Nat) → Nat → Nat
lift r n = if n == 0 then 0 else (r (n - 1)) + 1
```

Applying a renaming requires lifting it when going under a binder.

```haskell
rename :: (Nat → Nat) → Term → Term
rename r n = r n
rename r (b a) = (rename r b) (rename r a)
rename r (λ b) = λ (rename (lift r) b)
```

I denote substitution as `b{c/n}`, replacing the index `n` by `c` inside of `b`. Renaming by incrementing `1` is used when going under a binder so that the `c`'s zeroth indices don't get captured.

```haskell
n{c/m} = if n == m then c else n
(b a){c/m} = b{c/m} a{c/m}
(λ b){c/m} = let c' = rename (+ 1) c in λ (b{c'/m})
```