diff --git a/coq/AutosubstExtra.v b/coq/AutosubstExtra.v
index af2ad35..bc94dd2 100644
--- a/coq/AutosubstExtra.v
+++ b/coq/AutosubstExtra.v
@@ -1,5 +1,6 @@
 Require Import Omega.
 Require Import Autosubst.Autosubst.
+Require Import MyTactics. (* TEMPORARY *)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -167,3 +168,5 @@ Hint Extern 1 (_ = _) => autosubst : autosubst.
    metavariables, so the tactic [autosubst] fails. *)
 
 Hint Resolve scons_scomp : autosubst.
+
+(* -------------------------------------------------------------------------- *)
diff --git a/coq/Autosubst_EOS.v b/coq/Autosubst_EOS.v
new file mode 100644
index 0000000..846a79b
--- /dev/null
+++ b/coq/Autosubst_EOS.v
@@ -0,0 +1,329 @@
+Require Import Omega.
+Require Import Autosubst.Autosubst.
+Require Import AutosubstExtra. (* just for [upn_ren] *)
+Require Import MyTactics. (* TEMPORARY *)
+
+(* This file defines the construction [eos x t], which can be understood as
+   an end-of-scope mark for [x] in the term [t]. *)
+
+(* It also defines the single-variable substitution t.[u // x], which is the
+   substitution of [u] for [x] in [t]. *)
+
+(* -------------------------------------------------------------------------- *)
+
+Section EOS.
+
+Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
+
+(* The substitution [Var 0 .: Var 1 .: ... .: Var (x-1) .: Var (x+1) .: ...]
+   does not have [Var x] in its codomain. Thus, applying this substitution
+   to a term [t] can be understood as an end-of-scope construct: it means
+   ``end the scope of [x] in [t]''. We write [eos x t] for this construct.
+   It is also known as [adbmal]: see Hendriks and van Oostrom,
+   https://doi.org/10.1007/978-3-540-45085-6_11 *)
+
+(* There are at least two ways of defining the above substitution. One way
+   is to define it in terms of AutoSubst combinators: *)
+
+Definition eos_var x : var -> var :=
+  (iterate upren x (+1)).
+
+Definition eos x t :=
+  t.[ren (eos_var x)].
+
+Lemma eos_eq:
+  forall x t,
+  t.[upn x (ren (+1))] = eos x t.
+Proof.
+  intros. unfold eos, eos_var. erewrite upn_ren by tc. reflexivity.
+Qed.
+
+(* Another way is to define directly as a function of type [var -> var]. *)
+
+Definition lift_var x : var -> var :=
+  fun y => if le_gt_dec x y then 1 + y else y.
+
+(* The two definitions coincide: *)
+
+Lemma upren_lift_var:
+  forall x,
+  upren (lift_var x) = lift_var (S x).
+Proof.
+  intros. f_ext; intros [|y].
+  { reflexivity. }
+  { simpl. unfold lift_var, var. dblib_by_cases; omega. }
+Qed.
+
+Lemma eos_var_eq_lift_var:
+  eos_var = lift_var.
+Proof.
+  (* An uninteresting proof. *)
+  f_ext; intros x.
+  unfold eos_var.
+  induction x.
+  { reflexivity. }
+  { rewrite iterate_S.
+    rewrite IHx.
+    rewrite upren_lift_var.
+    reflexivity. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [eos] enjoys certain commutation laws. *)
+
+(* Ending the scope of variable [k], then the scope of variable [s], is the
+   same as first ending the scope of variable [1 + s], then ending the scope
+   of variable [k]. This holds provided [k <= s] is true, i.e., [k] is the
+   most recently-introduced variable.*)
+
+Lemma lift_var_lift_var:
+  forall k s,
+  k <= s ->
+  lift_var s >>> lift_var k = lift_var k >>> lift_var (S s).
+Proof.
+  (* By case analysis. *)
+  intros. f_ext; intros x. asimpl.
+  unfold lift_var, var. dblib_by_cases; omega.
+Qed.
+
+Lemma eos_eos:
+  forall k s t,
+  k <= s ->
+  eos k (eos s t) = eos (1 + s) (eos k t).
+Proof.
+  intros. unfold eos. asimpl.
+  rewrite eos_var_eq_lift_var.
+  rewrite lift_var_lift_var by eauto.
+  reflexivity.
+Qed.
+
+(* What about the case where [k] is the least recently-introduced variable?
+   It is obtained by symmetry, of course. *)
+
+Lemma eos_eos_reversed:
+  forall k s t,
+  k >= s + 1 ->
+  eos k (eos s t) = eos s (eos (k - 1) t).
+Proof.
+  intros.
+  replace k with (1 + (k - 1)) by omega.
+  rewrite <- eos_eos by omega.
+  replace (1 + (k - 1) - 1) with (k - 1) by omega.
+  reflexivity.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Single-variable substitutions. *)
+
+(* [subst_var u x] is the substitution of [u] for [x]. *)
+
+(* We give a direct definition of it as a function of type [var -> term],
+   defined by cases. I don't know if it could also be nicely defined in
+   terms of the basic combinators of de Bruijn algebra. Note that the
+   candidate definition [upn x (t .: ids)] is WRONG when [x > 0]. *)
+
+Definition subst_var (u : A) (x y : var) : A :=
+  match lt_eq_lt_dec y x with
+  | inleft (left _)  => ids y
+  | inleft (right _) => u
+  | inright _        => ids (y - 1)
+end.
+
+(* A nice notation: [t.[u // x]] is the substitution of [u] for [x] in [t]. *)
+
+Notation "t .[ u // x ]" := (subst (subst_var u x) t)
+  (at level 2, u at level 200, left associativity,
+   format "t .[ u // x ]") : subst_scope.
+
+(* The following laws serve as sanity checks: we got the definition right. *)
+
+Lemma subst_var_miss_1:
+  forall x y u,
+  y < x ->
+  (ids y).[u // x] = ids y.
+Proof.
+  intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
+Qed.
+
+Lemma subst_var_match:
+  forall x u,
+  (ids x).[ u // x ] = u.
+Proof.
+  intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
+Qed.
+
+Lemma subst_var_miss_2:
+  forall x y u,
+  x < y ->
+  (ids y).[u // x] = ids (y - 1).
+Proof.
+  intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
+Qed.
+
+(* In the special case where [x] is 0, the substitution [t // 0] can also
+   be written [t/], which is an AutoSubst notation for [t .: ids]. *)
+
+Lemma subst_var_0:
+  forall t u,
+  t.[u // 0] = t.[u/].
+Proof.
+  intros. f_equal. clear t.
+  f_ext. intros [|x].
+  { reflexivity. }
+  { unfold subst_var. simpl. f_equal. omega. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A cancellation law: substituting for a variable [x] that does not occur in
+   [t] yields just [t]. In other words, a substitution for [x] vanishes when
+   it reaches [eos x _]. *)
+
+(* In informal syntax, this lemma would be written:
+
+     t[u/x] = t
+
+   under the hypothesis that x does not occur free in t.
+
+   In de Bruijn style, the statement is just as short, and does not have a
+   side condition. Instead, it requires an explicit [eos x _] to appear at the
+   root of the term to which the substitution is applied; this may require
+   rewriting before this lemma can be applied. *)
+
+Lemma subst_eos:
+  forall x t u,
+  (eos x t).[u // x] = t.
+Proof.
+  intros.
+  (* Again, let's simplify this first. *)
+  unfold eos. asimpl.
+  (* Aha! We can forget about [t], and focus on proving that two
+     substitutions are equal. To do so, it is sufficient that
+     their actions on a variable [y] are the same. *)
+  rewrite <- subst_id.
+  f_equal. clear t.
+  f_ext. intro y.
+  (* The proof is easy if we replace [eos_var] with [lift_var]. *)
+  rewrite eos_var_eq_lift_var. simpl.
+  unfold subst_var, lift_var. dblib_by_cases; f_equal; omega.
+Qed.
+
+(* The above property allows us to prove that [eos x _] is injective.
+   Indeed, it has an inverse, namely [u // x], where [u] is arbitrary. *)
+
+Lemma eos_injective:
+  forall x t1 t2,
+  eos x t1 = eos x t2 ->
+  t1 = t2.
+Proof.
+  intros.
+  pose (u := t1). (* dummy *)
+  erewrite <- (subst_eos x t1 u).
+  erewrite <- (subst_eos x t2 u).
+  congruence.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* More commutation laws. *)
+
+Lemma eos_subst_1:
+  forall k s t u,
+  k <= s ->
+  eos k (t.[u // s]) = (eos k t).[eos k u // s + 1].
+Proof.
+  intros. unfold eos. asimpl. f_equal. clear t.
+  rewrite eos_var_eq_lift_var.
+  f_ext. intros y.
+  asimpl.
+  unfold subst_var, lift_var.
+  dblib_by_cases; asimpl; dblib_by_cases; solve [ eauto | f_equal; omega ].
+Qed.
+
+Lemma eos_subst_2:
+  forall k s t u,
+  s <= k ->
+  eos k (t.[u // s]) = (eos (k + 1) t).[eos k u // s].
+Proof.
+  intros. unfold eos. asimpl. f_equal. clear t.
+  rewrite eos_var_eq_lift_var.
+  f_ext. intros y.
+  asimpl.
+  unfold subst_var, lift_var.
+  dblib_by_cases; asimpl; dblib_by_cases; solve [ eauto | f_equal; omega ].
+Qed.
+
+Lemma subst_subst:
+  forall t k v s w,
+  k <= s ->
+  t.[w // k].[v // s] =
+  t.[eos k v // 1 + s].[w.[v // s] // k].
+Proof.
+  (* First, get rid of [t]. It is sufficient to consider the action of
+     these substitutions at a variable [y]. *)
+  intros. asimpl. f_equal. clear t. f_ext. intros y.
+  (* Replace [eos_var] with [lift_var], whose definition is more direct. *)
+  unfold eos. rewrite eos_var_eq_lift_var.
+  (* Then, use brute force (case analysis) to prove that the goal holds. *)
+  unfold subst_var. simpl.
+  dblib_by_cases; asimpl; dblib_by_cases;
+    (* This case analysis yields 5 cases, of which 4 are trivial... *)
+    eauto.
+  (* ... thus, one case remains. *)
+  (* Now get rid of [v]. It is again sufficient to consider the action
+     of these substitutions at a variable [z]. *)
+  replace v with v.[ids] at 1 by autosubst.
+  f_equal. f_ext. intros z. simpl.
+  (* Again, use brute force. *)
+  unfold lift_var. dblib_by_cases; f_equal. unfold var. omega.
+  (* Not really proud of this proof. *)
+Qed.
+
+Lemma pun_1:
+  forall t x,
+  (eos x t).[ ids x // x + 1 ] = t.
+Proof.
+  (* First, get rid of [t]. It is sufficient to consider the action of
+     these substitutions at a variable [y]. *)
+  intros. unfold eos. asimpl.
+  replace t with t.[ids] at 2 by autosubst.
+  f_equal. clear t. f_ext. intros y.
+  (* Replace [eos_var] with [lift_var], whose definition is more direct. *)
+  rewrite eos_var_eq_lift_var.
+  (* Then, use brute force (case analysis) to prove that the goal holds. *)
+  simpl. unfold subst_var, lift_var. dblib_by_cases; f_equal; unfold var; omega.
+Qed.
+
+Lemma pun_2:
+  forall t x,
+  (eos (x + 1) t).[ ids x // x ] = t.
+Proof.
+  (* First, get rid of [t]. It is sufficient to consider the action of
+     these substitutions at a variable [y]. *)
+  intros. unfold eos. asimpl.
+  replace t with t.[ids] at 2 by autosubst.
+  f_equal. clear t. f_ext. intros y.
+  (* Replace [eos_var] with [lift_var], whose definition is more direct. *)
+  rewrite eos_var_eq_lift_var.
+  (* Then, use brute force (case analysis) to prove that the goal holds. *)
+  simpl. unfold subst_var, lift_var. dblib_by_cases; f_equal; unfold var; omega.
+Qed.
+
+End EOS.
+
+(* Any notations defined in the above section must now be repeated. *)
+
+Notation "t .[ u // x ]" := (subst (subst_var u x) t)
+  (at level 2, u at level 200, left associativity,
+   format "t .[ u // x ]") : subst_scope.
+
+(* The tactic [subst_var] attempts to simplify applications of [subst_var]. *)
+
+Ltac subst_var :=
+  first [
+    rewrite subst_var_miss_1 by omega
+  | rewrite subst_var_match by omega
+  | rewrite subst_var_miss_2 by omega
+  ].
diff --git a/coq/Autosubst_Env.v b/coq/Autosubst_Env.v
new file mode 100644
index 0000000..83b702f
--- /dev/null
+++ b/coq/Autosubst_Env.v
@@ -0,0 +1,130 @@
+Require Import List.
+Require Import MyTactics. (* TEMPORARY *)
+Require Import Autosubst.Autosubst.
+Require Import Autosubst_EOS. (* [eos_var] *)
+
+(* Environments are sometimes represented as finite lists. This file
+   provides a few notions that helps deal with this representation. *)
+
+Section Env.
+
+Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The function [env2subst default], where [default] is a default value,
+   converts an environment (a finite list) to a substitution (a total
+   function). *)
+
+Definition env2subst (default : A) (e : list A) (x : var) : A :=
+  nth x e default.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [env_ren_comp e xi e'] means (roughly) that the environment [e] is equal to
+   the composition of the renaming [xi] and the environment [e'], that is,
+   [e = xi >>> e']. We also explicitly require the environments [e] and [e']
+   to have matching lengths, up to [xi], as this is *not* a consequence of
+   the other premise. *)
+
+Inductive env_ren_comp : list A -> (var -> var) -> list A -> Prop :=
+| EnvRenComp:
+    forall e xi e',
+    (forall x, x < length e -> xi x < length e') ->
+    (forall x default, nth x e default = nth (xi x) e' default) ->
+    env_ren_comp e xi e'.
+
+(* A reformulation of the second premise in the above definition. *)
+
+Lemma env_ren_comp_eq:
+  forall e xi e',
+  (forall default, env2subst default e = xi >>> env2subst default e') <->
+  (forall x default, nth x e default = nth (xi x) e' default).
+Proof.
+  unfold env2subst. split; intros h; intros.
+  { change (nth x e default) with ((fun x => nth x e default) x).
+    rewrite h. reflexivity. }
+  { f_ext; intro x. eauto. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Initialization: [e = id >>> e]. *)
+
+Lemma env_ren_comp_id:
+  forall e,
+  env_ren_comp e (fun x => x) e.
+Proof.
+  econstructor; eauto.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The relation [e = xi >>> e'] can be taken under a binder, as follows. *)
+
+Lemma env_ren_comp_up:
+  forall e xi e' v,
+  env_ren_comp e xi e' ->
+  env_ren_comp (v :: e) (upren xi) (v :: e').
+Proof.
+  inversion 1; intros; subst; econstructor;
+  intros [|x]; intros; simpl in *; eauto with omega.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* One element can be prepended to [e'], provided [xi] is adjusted. *)
+
+Lemma env_ren_comp_prepend:
+  forall e xi e' v,
+  env_ren_comp e xi e' ->
+  env_ren_comp e (xi >>> (+1)) (v :: e').
+Proof.
+  inversion 1; intros; subst.
+  econstructor; intros; simpl; eauto with omega.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A consequence of [env_ren_comp_id] and [env_ren_comp_prepend]. The renaming
+   (+1) will eat away the first entry in [v :: e]. *)
+
+Lemma env_ren_comp_plus1:
+  forall e v,
+  env_ren_comp e (+1) (v :: e).
+Proof.
+  econstructor; intros; simpl; eauto with omega.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* More generally, the renaming [eos_var x], which means that [x] goes out of
+   scope, will eat away the entry at index [x] in [e1 ++ v :: e2]. *)
+
+Lemma env_ren_comp_eos_var:
+  forall x e1 v e2,
+  x = length e1 ->
+  env_ren_comp (e1 ++ e2) (eos_var x) (e1 ++ v :: e2).
+Proof.
+  rewrite eos_var_eq_lift_var. unfold lift_var.
+  econstructor; intros y; dblib_by_cases.
+  { rewrite app_length in *. simpl. omega. }
+  { rewrite app_length in *. simpl. omega. }
+  { do 2 (rewrite app_nth2 by omega).
+    replace (1 + y - length e1) with (1 + (y - length e1)) by omega.
+    reflexivity. }
+  { do 2 (rewrite app_nth1 by omega).
+    reflexivity. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+End Env.
+
+Hint Resolve
+  env_ren_comp_id
+  env_ren_comp_up
+  env_ren_comp_prepend
+  env_ren_comp_plus1
+  env_ren_comp_eos_var
+: env_ren_comp.
diff --git a/coq/Autosubst_FreeVars.v b/coq/Autosubst_FreeVars.v
new file mode 100644
index 0000000..bf05011
--- /dev/null
+++ b/coq/Autosubst_FreeVars.v
@@ -0,0 +1,345 @@
+Require Import Omega.
+Require Import Autosubst.Autosubst.
+Require Import AutosubstExtra.
+Require Import Autosubst_EOS.
+
+(* -------------------------------------------------------------------------- *)
+
+Class IdsLemmas (term : Type) {Ids_term : Ids term} := {
+  (* The identity substitution is injective. *)
+  ids_inj:
+    forall x y,
+    ids x = ids y ->
+    x = y
+}.
+
+(* -------------------------------------------------------------------------- *)
+
+Section FreeVars.
+
+Context
+  {A : Type}
+  {Ids_A : Ids A}
+  {Rename_A : Rename A}
+  {Subst_A : Subst A}
+  {IdsLemmas_A : IdsLemmas A}
+  {SubstLemmas_A : SubstLemmas A}.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A reformulation of [ids_inj]. *)
+
+Lemma ids_inj_False:
+  forall x y,
+  ids x = ids y ->
+  x <> y ->
+  False.
+Proof.
+  intros.
+  assert (x = y). { eauto using ids_inj. }
+  unfold var in *.
+  omega.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The predicate [fv k t] means that the free variables of the term [t] are
+   contained in the semi-open interval [0..k). *)
+
+Definition fv k t :=
+  t.[upn k (ren (+1))] = t.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The predicate [closed t] means that the term [t] is closed, that is, [t]
+   has no free variables. *)
+
+Definition closed :=
+  fv 0.
+
+(* -------------------------------------------------------------------------- *)
+
+(* This technical lemma states that the renaming [+1] is injective. *)
+
+Lemma lift_inj_ids:
+  forall t x,
+  t.[ren (+1)] = ids (S x) <-> t = ids x.
+Proof.
+  split; intros.
+  { eapply lift_inj. autosubst. }
+  { subst. autosubst. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* This lemma characterizes the meaning of [fv k] when applied to a variable. *)
+
+Lemma fv_ids_eq:
+  forall k x,
+  fv k (ids x) <-> x < k.
+Proof.
+  unfold fv. induction k; intros.
+  (* Base case. *)
+  { asimpl. split; intros; elimtype False.
+    { eauto using ids_inj_False. }
+    { omega. }
+  }
+  (* Step. *)
+  { destruct x; asimpl.
+    { split; intros. { omega. } { reflexivity. } }
+    { rewrite lift_inj_ids.
+      rewrite <- id_subst.
+      rewrite IHk. omega. }
+  }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A simplification lemma. *)
+
+Lemma fv_lift:
+  forall k i t,
+  fv (k + i) t.[ren (+i)] <-> fv k t.
+Proof.
+  unfold fv. intros. asimpl.
+  rewrite Nat.add_comm.
+  rewrite <- upn_upn.
+  erewrite plus_upn by eauto.
+  rewrite <- subst_comp.
+  split; intros.
+  { eauto using lift_injn. }
+  { f_equal. eauto. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* If [t] has at most [n - 1] free variables,
+   and if [x] is inserted among them,
+   then we get [eos x t],
+   which has at most [n] free variables. *)
+
+Lemma fv_eos:
+  forall x n t,
+  x < n ->
+  fv (n - 1) t ->
+  fv n (eos x t).
+Proof.
+  unfold fv. intros x n t ? ht.
+  rewrite eos_eq in ht.
+  rewrite eos_eq.
+  rewrite eos_eos_reversed by omega. (* nice! *)
+  rewrite ht.
+  reflexivity.
+Qed.
+
+Lemma fv_eos_eq:
+  forall x n t,
+  x < n ->
+  fv n (eos x t) <->
+  fv (n - 1) t.
+Proof.
+  unfold fv. intros x n t ?.
+  rewrite eos_eq.
+  rewrite eos_eq.
+  rewrite eos_eos_reversed by omega. (* nice! *)
+  split; intros h.
+  { eauto using eos_injective. }
+  { rewrite h. reflexivity. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A substitution [sigma] is regular if and only if, for some [j], for
+   sufficiently large [x], [sigma x] is [x + j]. *)
+
+Definition regular (sigma : var -> A) :=
+  exists i j,
+  ren (+i) >> sigma = ren (+j).
+
+Lemma regular_ids:
+  regular ids.
+Proof.
+  exists 0. exists 0. autosubst.
+Qed.
+
+Lemma regular_plus:
+  forall i,
+  regular (ren (+i)).
+Proof.
+  intros. exists 0. exists i. autosubst.
+Qed.
+
+Lemma regular_upn:
+  forall n sigma,
+  regular sigma ->
+  regular (upn n sigma).
+Proof.
+  intros ? ? (i&j&hsigma).
+  exists (n + i). eexists (n + j).
+  replace (ren (+(n + i))) with (ren (+i) >> ren (+n)) by autosubst.
+  rewrite <- scompA.
+  rewrite up_liftn.
+  rewrite scompA.
+  rewrite hsigma.
+  autosubst.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* If the free variables of the term [t] are below [k], then [t] is unaffected
+   by a substitution of the form [upn k sigma]. *)
+
+(* Unfortunately, in this file, where the definition of type [A] is unknown, I
+   am unable to establish this result for arbitrary substitutions [sigma]. I
+   am able to establish it for *regular* substitutions, where The proof is somewhat interesting, so it is given here, even
+   though, once the definition of the type [A] is known, a more direct proof,
+   without a regularity hypothesis, can usually be given. *)
+
+(* An intermediate result states that, since [upn k (ren (+1))] does not
+   affect [t], then (by iteration) neither does [upn k (ren (+j))]. *)
+
+Lemma fv_unaffected_lift:
+  forall j t k,
+  fv k t ->
+  t.[upn k (ren (+j))] = t.
+Proof.
+  induction j as [| j ]; intros t k ht.
+  { asimpl. rewrite up_id_n. autosubst. }
+  { replace (ren (+S j)) with (ren (+1) >> ren (+j)) by autosubst.
+    rewrite <- up_comp_n.
+    replace (t.[upn k (ren (+1)) >> upn k (ren (+j))])
+       with (t.[upn k (ren (+1))].[upn k (ren (+j))]) by autosubst.
+    rewrite ht.
+    rewrite IHj by eauto.
+    eauto. }
+Qed.
+
+(* There follows that a substitution of the form [upn k sigma], where [sigma]
+   is regular, does not affect [t]. The proof is slightly subtle but very
+   short. The previous lemma is used twice. *)
+
+Lemma fv_unaffected_regular:
+  forall k t sigma,
+  fv k t ->
+  regular sigma ->
+  t.[upn k sigma] = t.
+Proof.
+  intros k t sigma ? (i&j&hsigma).
+  rewrite <- (fv_unaffected_lift i t k) at 1 by eauto.
+  asimpl. rewrite up_comp_n.
+  rewrite hsigma.
+  rewrite fv_unaffected_lift by eauto.
+  reflexivity.
+Qed.
+
+(* A corollary. *)
+
+Lemma closed_unaffected_regular:
+  forall t sigma,
+  closed t ->
+  regular sigma ->
+  t.[sigma] = t.
+Proof.
+  unfold closed. intros.
+  rewrite <- (upn0 sigma).
+  eauto using fv_unaffected_regular.
+Qed.
+
+(*One might also wish to prove a result along the following lines:
+
+  Goal
+    forall t k sigma1 sigma2,
+    fv k t ->
+    (forall x, x < k -> sigma1 x = sigma2 x) ->
+    t.[sigma1] = t.[sigma2].
+
+  I have not yet investigated how this could be proved. *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* If some term [t] has free variables under [j], then it also has free
+   variables under [k], where [j <= k]. *)
+
+Lemma fv_monotonic:
+  forall j k t,
+  fv j t ->
+  j <= k ->
+  fv k t.
+Proof.
+  intros. unfold fv.
+  replace k with (j + (k - j)) by omega.
+  rewrite <- upn_upn.
+  eauto using fv_unaffected_regular, regular_upn, regular_plus.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* These little lemmas may be occasionally useful. *)
+
+Lemma use_fv_length_cons:
+  forall A (x : A) (xs : list A) n t,
+  (forall x, fv (length (x :: xs)) t) ->
+  n = length xs ->
+  fv (n + 1) t.
+Proof.
+  intros. subst.
+  replace (length xs + 1) with (length (x :: xs)) by (simpl; omega).
+  eauto.
+Qed.
+
+Lemma prove_fv_length_cons:
+  forall A (x : A) (xs : list A) n t,
+  n = length xs ->
+  fv (n + 1) t ->
+  fv (length (x :: xs)) t.
+Proof.
+  intros. subst.
+  replace (length (x :: xs)) with  (length xs + 1) by (simpl; omega).
+  eauto.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [closed t] is equivalent to [t.[ren (+1)] = t]. *)
+
+Lemma closed_eq:
+  forall t,
+  closed t <-> t.[ren (+1)] = t.
+Proof.
+  unfold closed, fv. asimpl. tauto.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A variable is not closed. *)
+
+Lemma closed_ids:
+  forall x,
+  ~ closed (ids x).
+Proof.
+  unfold closed, fv. intros. asimpl. intro.
+  eauto using ids_inj_False.
+Qed.
+
+End FreeVars.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The tactic [fv] is intended to use a number of lemmas as rewriting rules.
+   The hint database [fv] can be extended with language-specific lemmas. *)
+
+Hint Rewrite @fv_ids_eq @fv_lift @fv_eos_eq : fv.
+
+Ltac fv :=
+  autorewrite with fv in *;
+  eauto with typeclass_instances.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A hint database to prove goals of the form [~ (closed _)] or [closed _]. *)
+
+Hint Resolve closed_ids : closed.
+
+(* -------------------------------------------------------------------------- *)
+
+Hint Resolve regular_ids regular_plus regular_upn : regular.
diff --git a/coq/ClosureConversion.v b/coq/ClosureConversion.v
new file mode 100644
index 0000000..208b3fd
--- /dev/null
+++ b/coq/ClosureConversion.v
@@ -0,0 +1,349 @@
+Require Import List.
+Require Import MyList.
+Require Import MyTactics.
+Require Import Sequences.
+Require Import LambdaCalculusSyntax.
+Require Import LambdaCalculusFreeVars.
+Require Import LambdaCalculusValues.
+Require Import LambdaCalculusBigStep.
+Require Import MetalSyntax.
+Require Import MetalBigStep.
+
+(* This file contains a definition of closure conversion and a proof of
+   semantic preservation. Closure conversion is a transformation of the
+   lambda-calculus into a lower-level calculus, nicknamed Metal, where
+   lambda-abstractions must be closed. *)
+
+(* The definition is slightly painful because we are using de Bruijn indices.
+   (That said, it is likely that using named variables would be painful too,
+   just in other ways.) One important pattern that we follow is that, as soon
+   as a variable [x] is no longer useful, we use [eos x _] to make it go out
+   of scope. Following this pattern is not just convenient -- it is actually
+   necessary. *)
+
+(* The main transformation function, [cc], has type [nat -> term -> metal]. If
+   [t] is a source term with [n] free variables, then [cc n t] is its image
+   under the transformation. *)
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* The auxiliary function [cc_lam n cct] defines the transformation of
+   the body of a lambda-abstraction. This auxiliary function must be isolated
+   because it is used twice, once within [cc], and once within [cc_value]. *)
+
+(* The parameter [n] is supposed to be the number of free variables of the
+   lambda-abstraction, and the parameter [cct] is the body of the transformed
+   lambda-abstraction. That is, [cct] is expected to be later instantiated
+   with [cc (n + 1) t], where [t] is the body of the source
+   lambda-abstraction. *)
+
+(* The term [cc_lam n cct] has just one free variable, namely 0, which
+   represents the formal parameter of the transformed lambda-abstraction. This
+   parameter is expected to be a pair [(clo, x)], where [clo] is the closure
+   and [x] is the formal parameter of the source lambda-abstraction. *)
+
+(* In nominal / informal syntax, the code would be roughly:
+
+     let (clo, x) = _ in
+     let x_1, ..., x_n = pi_1 clo, ..., pi_n clo in
+     cct
+
+*)
+
+(* We use meta-level [let] bindings, such as [let clo_x := 0 in ...].
+   These bindings generate no Metal code -- they should not be confused
+   with Metal [MLet] bindings. They are just a notational convenience. *)
+
+Definition cc_lam (n : nat) (cct : metal) : metal :=
+  (* Let us refer to variable 0 as [clo_x]. *)
+  let clo_x := 0 in
+  (* Initially, the variable [clo_x] is bound to a pair of [clo] and [x].
+     Decompose this pair, then let [clo_x] go out of scope. *)
+  MLetPair (* clo, x *) (MVar clo_x) (
+  let clo_x := clo_x + 2 in
+  eos clo_x (
+  (* Two variables are now in scope, namely [clo] and [x]. *)
+  let clo := 1 in
+  let x := 0 in
+  (* Now, bind [n] variables, informally referred to as [x_1, ..., x_n],
+     to the [n] tuple projections [pi_1 clo, ..., pi_n clo]. Then, let
+     [clo] go out of scope, as it is no longer needed. *)
+  MMultiLet 0 (MProjs n (MVar clo)) (
+  let clo := n + clo in
+  let x := n + x in
+  eos clo (
+  (* We need [x] to correspond to de Bruijn index 0. Currently, this is
+     not the case. So, rebind a new variable to [x], and let the old [x]
+     go out of scope. (Yes, this is a bit subtle.) We use an explicit
+     [MLet] binding, but in principle, could also use a substitution. *)
+  MLet (MVar x) (
+  let x := 1 + x in
+  eos x (
+  (* We are finally ready to enter the transformed function body. *)
+  cct
+  )))))).
+
+(* [cc] is the main transformation function. *)
+
+Fixpoint cc (n : nat) (t : term) : metal :=
+  match t with
+
+  | Var x =>
+      (* A variable is mapped to a variable. *)
+      MVar x
+
+  | Lam t =>
+      (* A lambda-abstraction [Lam t] is mapped to a closure, that is, a tuple
+         whose 0-th component is a piece of code (a closed lambda-abstraction)
+         and whose remaining [n] components are the [n] variables numbered 0,
+         1, ..., n-1. *)
+      MTuple (
+        MLam (cc_lam n (cc (n + 1) t)) ::
+        MVars n
+      )
+
+  | App t1 t2 =>
+      (* A function application is transformed into a closure invocation. *)
+      (* Bind [clo] to the closure produced by the (transformed) term [t1]. *)
+      MLet (cc n t1) (
+      let clo := 0 in
+      (* Bind [code] to the 0-th component of this closure. *)
+      MLet (MProj 0 (MVar clo)) (
+      let clo := 1 + clo in
+      let code := 0 in
+      (* Apply the function [code] to a pair of the closure and the value
+         produced by the (transformed) term [t2]. Note that both [clo] and
+         [code] must go out of scope before referring to [t2]. This could
+         be done in one step by applying the renaming [(+2)], but we prefer
+         to explicitly use [eos] twice, for greater clarity. *)
+      MApp
+        (MVar code)
+        (MPair
+           (MVar clo)
+           (eos clo (eos code (cc n t2)))
+        )
+      ))
+
+  | Let t1 t2 =>
+      (* A local definition is translated to a local definition. *)
+      MLet (cc n t1) (cc (n + 1) t2)
+
+  end.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* In order to prove that the above program transformation is sound (that is,
+   semantics-preserving), we must relate the values computed by the source
+   program with the values computed by the target program. Fortunately, the
+   relation is simple. (It is, in fact, a function.) The image of a source
+   closure [Clo t e] under the translation is a closure, represented as a
+   tuple, whose 0-th component is a lambda-abstraction -- the translation
+   of [Lam t] -- and whose remaining [n] components are the translation of
+   the environment [e]. *)
+
+Fixpoint cc_cvalue (cv : cvalue) : mvalue :=
+  match cv with
+  | Clo t e =>
+      let n := length e in
+      MVTuple (
+        MVLam (cc_lam n (cc (n + 1) t)) ::
+        map cc_cvalue e
+      )
+  end.
+
+(* The translation of environments is defined pointwise. *)
+
+Definition cc_cenv e :=
+  map cc_cvalue e.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* This lemma and hint increase the power of the tactic [length]. *)
+
+Lemma length_cc_env:
+  forall e,
+  length (cc_cenv e) = length e.
+Proof.
+  intros. unfold cc_cenv. length.
+Qed.
+
+Hint Rewrite length_cc_env : length.
+
+(* In this file, we allow [eauto with omega] to use the tactic [length]. *)
+
+Local Hint Extern 1 (_ = _ :> nat) => length : omega.
+Local Hint Extern 1 (lt _ _) => length : omega.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* We now check two purely syntactic properties of the transformation. First,
+   if the source program [t] has [n] free variables, then the transformed
+   program [cc n t] has [n] free variables, too. Second, in the transformed
+   program, every lambda-abstraction is closed. *)
+
+(* These proofs are "easy" and "routine", but could have been fairly lengthy
+   and painful if we had not set up appropriate lemmas and tactics, such as
+   [fv], beforehand. *)
+
+Lemma fv_cc_lam:
+  forall m n t,
+  fv (S n) t ->
+  1 <= m ->
+  fv m (cc_lam n t).
+Proof.
+  intros. unfold cc_lam. fv; length. repeat split;
+  eauto using fv_monotonic with omega.
+  { eapply fv_MProjs. fv. omega. }
+Qed.
+
+Lemma fv_cc:
+  forall t n1 n2,
+  fv n2 t ->
+  n1 = n2 ->
+  fv n1 (cc n2 t).
+Proof.
+  induction t; intros; subst; simpl; fv; unpack;
+  repeat rewrite Nat.add_1_r in *;
+  repeat split; eauto using fv_monotonic, fv_cc_lam with omega.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The following lemmas help reorganize our view of the environment. They are
+   typically used just before applying the lemma [mbigcbv_eos], that is, when
+   a variable [x] is about to go out of scope. We then want to organize the
+   environment so that it has the shape [e1 ++ mv :: e2], where the length of
+   [e1] is [x], so [mv] is the value that is dropped, and the environment
+   afterwards is [e1 ++ e2]. *)
+
+Local Lemma access_1:
+  forall {A} xs (x0 x : A),
+  x0 :: x :: xs = (x0 :: nil) ++ x :: xs.
+Proof.
+  reflexivity.
+Qed.
+
+Local Lemma access_2:
+  forall {A} xs (x0 x1 x : A),
+  x0 :: x1 :: x :: xs = (x0 :: x1 :: nil) ++ x :: xs.
+Proof.
+  reflexivity.
+Qed.
+
+Local Lemma access_n_plus_1:
+  forall {A} xs (x : A) ys,
+  xs ++ x :: ys = (xs ++ x :: nil) ++ ys.
+Proof.
+  intros. rewrite <- app_assoc. reflexivity.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* We now establish a (forward) semantic preservation statement: if under
+   environment [e] the source term [t] computes the value [cv], then under
+   the translation of [e], the translation of [t] computes the translation
+   of [cv]. *)
+
+(* The proof is fairly routine and uninteresting; it is just a matter of
+   checking that everything works as expected. A crucial point that helps
+   keep the proof manageable is that we have defined auxiliary evaluation
+   lemmas for tuples, projections, [MMultiLet], and so on. *)
+
+(* Although the proof is not "hard", it would be difficult to do by hand, as
+   it is quite deep and one must keep track of many details, such as the shape
+   of the runtime environment at every program point -- that is, which de
+   Bruijn index is bound to which value. An off-by-one error in a de Bruijn
+   index, or a list that is mistakenly reversed, would be difficult to detect
+   in a handwritten proof. Machine assistance is valuable in this kind of
+   exercise. *)
+
+Theorem semantic_preservation:
+  forall e t cv,
+  ebigcbv e t cv ->
+  forall n,
+  n = length e ->
+  mbigcbv (cc_cenv e) (cc n t) (cc_cvalue cv).
+Proof.
+  induction 1; intros; simpl.
+
+  (* Case: [Var]. Nothing much to say; apply the evaluation rule and
+     check that its side conditions hold. *)
+  { econstructor.
+    { length. }
+    { subst cv.
+      erewrite (nth_indep (cc_cenv e)) by length.
+      unfold cc_cenv. rewrite map_nth. eauto. }
+  }
+
+  (* Case: [Lam]. We have to check that a transformed lambda-abstraction
+     (as per [cc]) evaluates to a transformed closure (as per [cc_value]).
+     This is fairly easy. *)
+  { subst. econstructor.
+    (* The code component. We must check that it is closed. *)
+    { econstructor.
+      assert (fv (length e + 1) t).
+      { eapply (use_fv_length_cons _ dummy_cvalue); eauto. }
+      unfold closed. fv. eauto using fv_cc_lam, fv_cc with omega. }
+    (* The remaining components. *)
+    { eapply MBigcbvTuple.
+      rewrite <- length_cc_env. eauto using MBigcbvVars. }
+  }
+
+  (* Case: [App]. This is where most of the action takes place. We must
+     essentially "execute" the calling sequence and check that it works
+     as expected. *)
+
+  { (* Evaluate the first [Let], which binds a variable [clo] to the closure. *)
+    econstructor. { eauto. }
+    (* Evaluate the second [Let], which projects the code out of the closure,
+       and binds the variable [code]. *)
+    econstructor.
+    { econstructor; [| eauto ].
+      econstructor; simpl; eauto with omega. }
+    (* We are now looking at a function application. Evaluate in turn the function,
+       its actual argument, and the call itself. *)
+    econstructor.
+    (* The function. *)
+    { econstructor; simpl; eauto with omega. }
+    (* Its argument. *)
+    { econstructor.
+      { econstructor; simpl; eauto with omega. }
+      { (* Skip two [eos] constructs. *)
+        rewrite access_1. eapply mbigcbv_eos; [ simpl | length ].
+        eapply mbigcbv_eos with (e1 := nil); [ simpl | length ].
+        eauto. }
+    }
+    (* The call itself. Here, we step into a transformed lambda-abstraction, and
+       we begin studying how it behaves when executed. *)
+    unfold cc_lam at 2.
+    (* Evaluate [MLetPair], which binds [clo] and [x]. *)
+    eapply MBigcbvLetPair.
+    { econstructor; simpl; eauto with omega. }
+    (* Skip [eos]. *)
+    rewrite access_2. eapply mbigcbv_eos; [ simpl | eauto ].
+    (* Evaluate [MMultiLet]. *)
+    eapply MBigcbvMultiLetProjs.
+    { econstructor; simpl; eauto with omega. }
+    { length. }
+    (* Skip [eos]. *)
+    rewrite access_n_plus_1. eapply mbigcbv_eos; [| length ].
+    rewrite app_nil_r, Nat.add_0_r.
+    (* Evaluate the new binding of [x]. *)
+    econstructor.
+    { econstructor.
+      { length. }
+      { rewrite app_nth by (rewrite map_length; omega). simpl. eauto. }
+    }
+    (* Skip [eos]. *)
+    rewrite app_comm_cons. eapply mbigcbv_eos; [ rewrite app_nil_r | length ].
+    (* Evaluate the function body. *)
+    eauto with omega. }
+
+  (* Case: [Let]. Immediate. *)
+  { econstructor; eauto with omega. }
+
+Qed.
diff --git a/coq/LambdaCalculusFreeVars.v b/coq/LambdaCalculusFreeVars.v
index 1d5fdbb..423d1d6 100644
--- a/coq/LambdaCalculusFreeVars.v
+++ b/coq/LambdaCalculusFreeVars.v
@@ -14,12 +14,6 @@ Qed.
 
 (* -------------------------------------------------------------------------- *)
 
-(* The predicate [fv k t] means that the free variables of the term [t] are
-   contained in the semi-open interval [0..k). *)
-
-Definition fv k t :=
-  t.[upn k (ren (+1))] = t.
-
 (* The predicate [fv] is characterized by the following lemmas. *)
 
 Lemma fv_Var_eq:
@@ -67,28 +61,8 @@ Qed.
 
 Hint Rewrite fv_Var_eq fv_Lam_eq fv_App_eq fv_Let_eq : fv.
 
-(* The tactic [fv] uses the above lemmas as rewriting rules. *)
-
-Ltac fv :=
-  autorewrite with fv in *.
-
 (* -------------------------------------------------------------------------- *)
 
-(* The predicate [closed t] means that the term [t] is closed, that is, [t]
-   has no free variables. *)
-
-Definition closed :=
-  fv 0.
-
-(* [closed t] is equivalent to [lift 1 t = t]. *)
-
-Lemma closed_eq:
-  forall t,
-  closed t <-> lift 1 t = t.
-Proof.
-  unfold closed, fv. asimpl. tauto.
-Qed.
-
 (* The following lemmas allow decomposing a closedness hypothesis.
    Because [closed] is not an inductive notion, there is no lemma
    for [Lam] and for the right-hand side of [Let]. *)
diff --git a/coq/LambdaCalculusSyntax.v b/coq/LambdaCalculusSyntax.v
index 56d1898..0134bad 100644
--- a/coq/LambdaCalculusSyntax.v
+++ b/coq/LambdaCalculusSyntax.v
@@ -3,6 +3,8 @@ Require Import MyTactics.
 Require Export Autosubst.Autosubst.
 Require Export AutosubstExtra.
 Require Export Autosubst_IsRen.
+(* Require Export Autosubst_EOS. *)
+Require Export Autosubst_FreeVars.
 
 (* The syntax of the lambda-calculus. *)
 
@@ -18,6 +20,9 @@ Instance Rename_term : Rename term. derive. Defined.
 Instance Subst_term : Subst term. derive. Defined.
 Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
+Instance IdsLemmas_term : IdsLemmas term.
+Proof. econstructor. intros. injections. eauto. Qed.
+
 (* If the image of [t] through a substitution is a variable, then [t] must
    itself be a variable. *)
 
diff --git a/coq/MetaBigStep.v b/coq/MetaBigStep.v
new file mode 100644
index 0000000..e69de29
diff --git a/coq/MetalBigStep.v b/coq/MetalBigStep.v
new file mode 100644
index 0000000..6f0632b
--- /dev/null
+++ b/coq/MetalBigStep.v
@@ -0,0 +1,313 @@
+Require Import List.
+Require Import MyList.
+Require Import MyTactics.
+Require Import Sequences.
+Require Import MetalSyntax.
+Require Import Autosubst_Env.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* A big-step call-by-value semantics with explicit environments. *)
+
+(* Because every lambda-abstraction is closed, no closures are involved:
+   a lambda-abstraction evaluates to itself. Thus, an mvalue [mv] must be
+   either a (closed) lambda-abstraction or a pair of mvalues. *)
+
+Inductive mvalue :=
+| MVLam  : {bind metal} -> mvalue
+| MVPair : mvalue -> mvalue -> mvalue.
+
+Definition dummy_mvalue : mvalue :=
+  MVLam (MVar 0).
+
+(* An environment [e] is a list of mvalues. *)
+
+Definition menv :=
+  list mvalue.
+
+(* The judgement [mbigcbv e t mv] means that, under the environment [e], the
+   term [t] evaluates to [mv]. *)
+
+Inductive mbigcbv : menv -> metal -> mvalue -> Prop :=
+| MBigcbvVar:
+    forall e x mv,
+    (* The variable [x] must be in the domain of [e]. *)
+    x < length e ->
+    (* This allows us to safely look up [e] at [x]. *)
+    mv = nth x e dummy_mvalue ->
+    mbigcbv e (MVar x) mv
+| MBigcbvLam:
+    forall e t,
+    (* The lambda-abstraction must have no free variables. *)
+    closed (MLam t) ->
+    mbigcbv e (MLam t) (MVLam t)
+| MBigcbvApp:
+    forall e t1 t2 u1 mv2 mv,
+    (* Evaluate [t1] to a lambda-abstraction, *)
+    mbigcbv e t1 (MVLam u1) ->
+    (* evaluate [t2] to a value, *)
+    mbigcbv e t2 mv2 ->
+    (* and evaluate the function body in a singleton environment. *)
+    mbigcbv (mv2 :: nil) u1 mv ->
+    mbigcbv e (MApp t1 t2) mv
+| MBigcbvLet:
+    forall e t1 t2 mv1 mv,
+    (* Evaluate [t1] to a value, *)
+    mbigcbv e t1 mv1 ->
+    (* and evaluate [t2] under a suitable environment. *)
+    mbigcbv (mv1 :: e) t2 mv ->
+    mbigcbv e (MLet t1 t2) mv
+| MBigcbvPair:
+    forall e t1 t2 mv1 mv2,
+    (* Evaluate each component to a value, *)
+    mbigcbv e t1 mv1 ->
+    mbigcbv e t2 mv2 ->
+    (* and construct a pair. *)
+    mbigcbv e (MPair t1 t2) (MVPair mv1 mv2)
+| MBigcbvPi:
+    forall e i t mv1 mv2 mv,
+    (* Evaluate [t] to a pair value, *)
+    mbigcbv e t (MVPair mv1 mv2) ->
+    (* and project out the desired component. *)
+    mv = match i with 0 => mv1 | _ => mv2 end ->
+    mbigcbv e (MPi i t) mv
+.
+
+Hint Constructors mbigcbv : mbigcbv.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A reformulation of the evaluation rule for variables. *)
+
+Lemma MBigcbvVarExact:
+  forall e1 mv e2 x,
+  x = length e1 ->
+  mbigcbv (e1 ++ mv :: e2) (MVar x) mv.
+Proof.
+  intros. econstructor.
+  { length. }
+  { rewrite app_nth by eauto. reflexivity. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* We now examine how the big-step semantics interacts with renamings.
+   We prove that if (roughly) the equation [e = xi >>> e'] holds then
+   evaluating [t.[xi]] under [e'] is the same as evaluating [t] under
+   [e]. *)
+
+Lemma mbigcbv_ren:
+  forall e t mv,
+  mbigcbv e t mv ->
+  forall e' xi,
+  env_ren_comp e xi e' ->
+  mbigcbv e' t.[ren xi] mv.
+Proof.
+  induction 1; intros;
+  try solve [ asimpl; eauto with env_ren_comp mbigcbv ].
+  (* MVar *)
+  { pick @env_ren_comp invert.
+    econstructor; eauto. }
+  (* MLam *)
+  { rewrite closed_unaffected by eauto.
+    eauto with mbigcbv. }
+Qed.
+
+(* As a special case, evaluating [eos x t] under an environment of the form
+   [e1 ++ mv :: e2], where length of [e1] is [x] (so [x] is mapped to [mv])
+   is the same as evaluating [t] under [e1 ++ e2]. The operational effect
+   of the end-of-scope mark [eos x _] is to delete the value stored at index
+   [x] in the evaluation environment. *)
+
+Lemma mbigcbv_eos:
+  forall e1 e2 x t mv mw,
+  mbigcbv (e1 ++ e2) t mw ->
+  x = length e1 ->
+  mbigcbv (e1 ++ mv :: e2) (eos x t) mw.
+Proof.
+  intros. eapply mbigcbv_ren; eauto with env_ren_comp.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* Evaluation rules for (simulated) tuples. *)
+
+Fixpoint MVTuple mvs :=
+  match mvs with
+  | nil =>
+      MVLam (MVar 0)
+  | mv :: mvs =>
+      MVPair mv (MVTuple mvs)
+  end.
+
+Lemma MBigcbvTuple:
+  forall e ts mvs,
+  (* Evaluate every component to a value, *)
+  Forall2 (mbigcbv e) ts mvs ->
+  (* and construct a tuple. *)
+  mbigcbv e (MTuple ts) (MVTuple mvs).
+Proof.
+  induction 1; simpl; econstructor; eauto.
+  { unfold closed. fv. }
+Qed.
+
+Lemma MBigcbvProj:
+  forall i e t mvs mv,
+  i < length mvs ->
+  (* Evaluate [t] to a tuple value, *)
+  mbigcbv e t (MVTuple mvs) ->
+  (* and project out the desired component. *)
+  mv = nth i mvs dummy_mvalue ->
+  mbigcbv e (MProj i t) mv.
+Proof.
+  (* By induction on [i]. In either case, [mvs] cannot be an empty list. *)
+  induction i; intros; (destruct mvs as [| mv0 mvs ]; [ false; simpl in *; omega |]).
+  (* Base case. *)
+  { econstructor; eauto. }
+  (* Step case. *)
+  { assert (i < length mvs). { length. }
+    simpl. eauto with mbigcbv. }
+Qed.
+
+Lemma MBigcbvLetPair:
+  forall e t u mv mv1 mv2,
+  mbigcbv e t (MVPair mv1 mv2) ->
+  mbigcbv (mv2 :: mv1 :: e) u mv ->
+  mbigcbv e (MLetPair t u) mv.
+Proof.
+  unfold MLetPair. eauto 6 using mbigcbv_ren, env_ren_comp_plus1 with mbigcbv.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* Evaluation rules for [MMultiLet]. *)
+
+Local Lemma Forall2_mbigcbv_plus1:
+  forall ts mvs e i mv,
+  Forall2 (mbigcbv e) (map (fun t : metal => lift i t) ts) mvs ->
+  Forall2 (mbigcbv (mv :: e)) (map (fun t : metal => lift (i + 1) t) ts) mvs.
+Proof.
+  induction ts as [| t ts]; simpl; intros;
+  pick Forall2 invert; econstructor; eauto.
+  replace (lift (i + 1) t) with (lift 1 (lift i t)) by autosubst.
+  eauto using mbigcbv_ren, env_ren_comp_plus1.
+Qed.
+
+Lemma MBigcbvMultiLet:
+  forall ts e i u mvs mv,
+  Forall2 (mbigcbv e) (map (fun t => lift i t) ts) mvs ->
+  mbigcbv (rev mvs ++ e) u mv ->
+  mbigcbv e (MMultiLet i ts u) mv.
+Proof.
+  induction ts; simpl; intros; pick Forall2 invert.
+  { eauto. }
+  { pick mbigcbv ltac:(fun h => rewrite rev_cons_app in h).
+    econstructor; eauto using Forall2_mbigcbv_plus1. }
+Qed.
+
+Lemma MBigcbvMultiLet_0:
+  forall ts e u mvs mv,
+  Forall2 (mbigcbv e) ts mvs ->
+  mbigcbv (rev mvs ++ e) u mv ->
+  mbigcbv e (MMultiLet 0 ts u) mv.
+Proof.
+  intros. eapply MBigcbvMultiLet.
+  { asimpl. rewrite map_id. eauto. }
+  { eauto. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* An evaluation rule for [MVars]. *)
+
+Lemma MBigcbvVars_preliminary:
+  forall e2 e1 e x n,
+  e = e1 ++ e2 ->
+  x = length e1 ->
+  n = length e2 ->
+  Forall2 (mbigcbv e) (map MVar (seq x n)) e2.
+Proof.
+  induction e2 as [| mv e2 ]; intros; subst; econstructor.
+  { eauto using MBigcbvVarExact. }
+  { eapply IHe2 with (e1 := e1 ++ mv :: nil).
+    { rewrite <- app_assoc. reflexivity. }
+    { length. }
+    { eauto. }
+  }
+Qed.
+
+Lemma MBigcbvVars:
+  forall e,
+  Forall2 (mbigcbv e) (MVars (length e)) e.
+Proof.
+  unfold MVars, nats. intros.
+  eapply MBigcbvVars_preliminary with (e1 := nil); eauto.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* An evaluation rule for [MProjs]. If the term [t] evaluates to a tuple whose
+   components numbered 1, ..., n are collected in the list [mvs1], then the
+   family of terms [MProjs n t] evaluates to the family of values [rev mvs1]. *)
+
+Lemma MBigcbvProjs:
+  forall n e t mv mvs1 mvs2,
+  mbigcbv e t (MVTuple (mv :: mvs1 ++ mvs2)) ->
+  length mvs1 = n ->
+  Forall2 (mbigcbv e) (MProjs n t) (rev mvs1).
+Proof.
+  (* This result is "obvious" but requires some low-level work. *)
+  unfold MProjs. induction n; intros.
+  (* Case: [n] is zero. Then, [mvs1] must be [nil]. The result follows. *)
+  { destruct mvs1; [| false; simpl in *; omega ].
+    econstructor. }
+  (* Case: [n] is nonzero. Then, the list [mvs1] must be nonempty. *)
+  assert (hmvs1: mvs1 <> nil).
+  { intro. subst. simpl in *. omega. }
+  (* So, this list has one element at the end. Let us write this list in the
+     form [mvs1 ++ mv1]. *)
+  destruct (exists_last hmvs1) as (hd&mv1&?). subst mvs1. clear hmvs1.
+  generalize dependent hd; intro mvs1; intros.
+  (* Simplify. *)
+  rewrite rev_unit.
+  rewrite <- app_assoc in *.
+  rewrite app_length in *.
+  assert (length mvs1 = n). { length. }
+  simpl map.
+  econstructor.
+  (* The list heads. *)
+  { eapply MBigcbvProj; eauto.
+    { length. }
+    { replace (n + 1) with (S n) by omega. simpl.
+      rewrite app_nth by omega.
+      reflexivity. }
+  }
+  (* The list tails. *)
+  { eauto. }
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* An evaluation rule for the combination of [MMultiLet] and [MProjs]. If the
+   term [t] evaluates to a tuple whose components are [mv :: mvs], and if [n]
+   is the length of [mvs], then evaluating [MMultiLet 0 (MProjs n t) u] in an
+   environment [e] leads to evaluating [u] in environment [mvs ++ e]. *)
+
+Lemma MBigcbvMultiLetProjs:
+  forall e t mvs u mv mw n,
+  mbigcbv e t (MVTuple (mv :: mvs)) ->
+  length mvs = n ->
+  mbigcbv (mvs ++ e) u mw ->
+  mbigcbv e (MMultiLet 0 (MProjs n t) u) mw.
+Proof.
+  intros.
+  eapply MBigcbvMultiLet_0.
+  { eapply MBigcbvProjs with (mvs2 := nil); [ rewrite app_nil_r |]; eauto. }
+  { rewrite rev_involutive. eauto. }
+Qed.
diff --git a/coq/MetalSyntax.v b/coq/MetalSyntax.v
new file mode 100644
index 0000000..f846e20
--- /dev/null
+++ b/coq/MetalSyntax.v
@@ -0,0 +1,432 @@
+Require Import List.
+Require Import MyList.
+Require Import MyTactics.
+Require Export Autosubst.Autosubst.
+Require Export AutosubstExtra.
+Require Export Autosubst_EOS.
+Require Export Autosubst_FreeVars.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Metal is a lambda-calculus where every lambda-abstractions must be closed.
+   It is equipped with pairs and projections. It is intended to serve as the
+   target of closure conversion. *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* Syntax. *)
+
+Inductive metal :=
+| MVar  : var -> metal
+| MLam  : {bind metal} -> metal
+| MApp  : metal -> metal -> metal
+| MLet  : metal -> {bind metal} -> metal
+| MPair : metal -> metal -> metal
+| MPi   : nat -> metal -> metal
+.
+
+Instance Ids_metal : Ids metal. derive. Defined.
+Instance Rename_metal : Rename metal. derive. Defined.
+Instance Subst_metal : Subst metal. derive. Defined.
+Instance SubstLemmas_metal : SubstLemmas metal. derive. Qed.
+
+Instance IdsLemmas_metal : IdsLemmas metal.
+Proof. econstructor. intros. injections. eauto. Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* We equip the calculus with pairs, instead of general tuples, because
+   this makes life in Coq simpler -- we would otherwise have an occurrence
+   of [list metal] in the definition of [metal], and would need to ask for
+   a custom induction scheme. *)
+
+(* Instead, we simulate tuples using nested pairs. This would of course be
+   inefficient in real life, but fur our purposes, should be fine. *)
+
+Fixpoint MTuple ts :=
+  match ts with
+  | nil =>
+      (* A dummy value serves as the tail. *)
+      MLam (MVar 0)
+  | t :: ts =>
+      MPair t (MTuple ts)
+  end.
+
+Fixpoint MProj i t :=
+  match i with
+  | 0 =>
+      (* Take the left pair component. *)
+      MPi 0 t
+  | S i =>
+      (* Take the right pair component and continue. *)
+      MProj i (MPi 1 t)
+  end.
+
+Definition MLetPair t u :=
+  MLet (* x_0 = *) (MPi 0 t) (
+    MLet (* x_1 = *) (MPi 1 (lift 1 t))
+      u
+  ).
+
+(* -------------------------------------------------------------------------- *)
+
+(* [MMultiLet 0 ts u] is a sequence of [MLet] bindings. [n] variables, where
+   [n] is [length ts], are bound to the terms [ts] in the term [u]. The
+   recursive structure of the definition is such that the *last* term in the
+   list [ts] is bound *last*, hence is referred to as variable 0 in [u]. *)
+
+Fixpoint MMultiLet i ts u :=
+  match ts with
+  | nil =>
+      u
+  | t :: ts =>
+      MLet (lift i t) (MMultiLet (i + 1) ts u)
+  end.
+
+(* The auxiliary parameter [i] in [MMultiLet i ts u] is required for the
+   recursive definition to go through, but, as far as the end user is
+   concerned, is not very useful. It can be eliminated as follows. *)
+
+Lemma MMultiLet_ij:
+  forall ts delta i j u,
+  i + delta = j ->
+  MMultiLet j ts u = MMultiLet i (map (fun t => lift delta t) ts) u.
+Proof.
+  induction ts; intros; simpl; eauto.
+  f_equal.
+  { asimpl. congruence. }
+  { erewrite IHts. eauto. omega. }
+Qed.
+
+Lemma MMultiLet_i0:
+  forall i ts u,
+  MMultiLet i ts u = MMultiLet 0 (map (fun t => lift i t) ts) u.
+Proof.
+  eauto using MMultiLet_ij with omega.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [MVars n] is the list [MVar 0, ..., MVar (n-1)]. *)
+
+Definition MVars (n : nat) : list metal :=
+  map MVar (nats n).
+
+(* -------------------------------------------------------------------------- *)
+
+(* [MProjs n t] is the list [MProj n t, ..., MProj 1 t]. *)
+
+Definition MProjs (n : nat) (t : metal) :=
+  map (fun i => MProj (i + 1) t) (rev_nats n).
+
+(* This list has length [n]. *)
+
+Lemma length_MProjs:
+  forall n t,
+  length (MProjs n t) = n.
+Proof.
+  unfold MProjs. intros. rewrite map_length, length_rev_nats. eauto.
+Qed.
+
+Hint Rewrite length_MProjs : length.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Substitution (boilerplate lemmas). *)
+
+Lemma subst_MVar:
+  forall x sigma,
+  (MVar x).[sigma] = sigma x.
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma subst_MLam:
+  forall t sigma,
+  (MLam t).[sigma] = MLam t.[up sigma].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma subst_MApp:
+  forall t1 t2 sigma,
+  (MApp t1 t2).[sigma] = MApp t1.[sigma] t2.[sigma].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma subst_MLet:
+  forall t1 t2 sigma,
+  (MLet t1 t2).[sigma] = MLet t1.[sigma] t2.[up sigma].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma subst_MPair:
+  forall t1 t2 sigma,
+  (MPair t1 t2).[sigma] = MPair t1.[sigma] t2.[sigma].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma subst_MPi:
+  forall i t sigma,
+  (MPi i t).[sigma] = MPi i t.[sigma].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma subst_MTuple:
+  forall ts sigma,
+  (MTuple ts).[sigma] = MTuple (map (subst sigma) ts).
+Proof.
+  induction ts; intros; asimpl; [ | rewrite IHts ]; reflexivity.
+Qed.
+
+Lemma subst_MProj:
+  forall n t sigma,
+  (MProj n t).[sigma] = MProj n t.[sigma].
+Proof.
+  induction n; intros; asimpl; [ | rewrite IHn ]; autosubst.
+Qed.
+
+Lemma subst_MLetPair:
+  forall t u sigma,
+  (MLetPair t u).[sigma] = MLetPair t.[sigma] u.[upn 2 sigma].
+Proof.
+  unfold MLetPair. intros. autosubst.
+Qed.
+
+Lemma subst_MMultiLet:
+  forall ts i u sigma,
+  (MMultiLet i ts u).[upn i sigma] =
+  MMultiLet i (map (subst sigma) ts) u.[upn (length ts) (upn i sigma)].
+Proof.
+  induction ts; intros; asimpl; f_equal.
+  { erewrite plus_upn by tc. eauto. }
+  { rewrite IHts.
+    repeat erewrite upn_upn by tc.
+    do 3 f_equal. omega. }
+Qed.
+
+Lemma subst_MMultiLet_0:
+  forall ts u sigma,
+  (MMultiLet 0 ts u).[sigma] =
+  MMultiLet 0 (map (subst sigma) ts) u.[upn (length ts) sigma].
+Proof.
+  intros.
+  change sigma with (upn 0 sigma) at 1.
+  eapply subst_MMultiLet.
+Qed.
+
+Lemma subst_MVars:
+  forall n sigma,
+  map (subst sigma) (MVars n) = map sigma (nats n).
+Proof.
+  intros. unfold MVars. rewrite map_map. reflexivity.
+Qed.
+
+Lemma subst_MProjs:
+  forall n t sigma,
+  map (subst sigma) (MProjs n t) = MProjs n t.[sigma].
+Proof.
+  unfold MProjs. induction n; intros; simpl; eauto.
+  rewrite subst_MProj, IHn. eauto.
+Qed.
+
+Hint Rewrite
+  subst_MVar subst_MLam subst_MApp subst_MLet subst_MPair subst_MPi
+  subst_MTuple subst_MProj subst_MLetPair
+  subst_MMultiLet subst_MMultiLet_0
+  subst_MVars subst_MProjs
+: subst.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Free variables (boilerplate lemmas). *)
+
+Lemma fv_MVar:
+  forall x k,
+  fv k (MVar x) <-> x < k.
+Proof.
+  eauto using fv_ids_eq.
+Qed.
+
+Ltac prove_fv :=
+  unfold fv; intros; asimpl;
+  split; intros; unpack; [ injections | f_equal ]; eauto.
+
+Lemma fv_MLam:
+  forall t k,
+  fv k (MLam t) <-> fv (k + 1) t.
+Proof.
+  prove_fv.
+Qed.
+
+Lemma fv_MApp:
+  forall t1 t2 k,
+  fv k (MApp t1 t2) <-> fv k t1 /\ fv k t2.
+Proof.
+  prove_fv.
+Qed.
+
+Lemma fv_MLet:
+  forall t1 t2 k,
+  fv k (MLet t1 t2) <-> fv k t1 /\ fv (k + 1) t2.
+Proof.
+  prove_fv.
+Qed.
+
+Lemma fv_MPair:
+  forall t1 t2 k,
+  fv k (MPair t1 t2) <-> fv k t1 /\ fv k t2.
+Proof.
+  prove_fv.
+Qed.
+
+Lemma fv_MPi:
+  forall i t k,
+  fv k (MPi i t) <-> fv k t.
+Proof.
+  prove_fv.
+Qed.
+
+Hint Rewrite fv_MVar fv_MLam fv_MApp fv_MLet fv_MPair fv_MPi : fv.
+
+Lemma fv_MTuple:
+  forall k ts,
+  fv k (MTuple ts) <-> Forall (fv k) ts.
+Proof.
+  induction ts; simpl; intros; fv; split; intros; unpack.
+  { econstructor. }
+  { omega. }
+  { rewrite IHts in *. econstructor; eauto. }
+  { rewrite IHts in *. pick Forall invert. eauto. }
+Qed.
+
+Lemma fv_MProj:
+  forall k n t,
+  fv k (MProj n t) <-> fv k t.
+Proof.
+  induction n; intros; simpl; [ | rewrite IHn ]; fv; tauto.
+Qed.
+
+Lemma fv_MLetPair:
+  forall k t u,
+  fv k (MLetPair t u) <-> fv k t /\ fv (k + 2) u.
+Proof.
+  intros. unfold MLetPair. fv; tc.
+  replace (k + 1 + 1) with (k + 2) by omega.
+  tauto.
+Qed.
+
+Local Lemma MLet_inj:
+  forall t1 u1 t2 u2,
+  MLet t1 u1 = MLet t2 u2 <-> t1 = t2 /\ u1 = u2.
+Proof.
+  split; intros; injections; unpack; subst; eauto.
+Qed.
+
+Local Lemma cons_cons_eq:
+  forall {A} (x1 x2 : A) xs1 xs2,
+  x1 :: xs1 = x2 :: xs2 <->
+  x1 = x2 /\ xs1 = xs2.
+Proof.
+  split; intros; injections; unpack; subst; eauto.
+Qed.
+
+Local Lemma MMultiLet_inj:
+  forall ts1 u1 ts2 u2 i,
+  length ts1 = length ts2 ->
+  MMultiLet i ts1 u1 = MMultiLet i ts2 u2 <->
+  ts1 = ts2 /\ u1 = u2.
+Proof.
+  induction ts1; destruct ts2; intros; simpl;
+  try solve [ false; simpl in *; omega ].
+  { tauto. }
+  { rewrite MLet_inj.
+    rewrite lift_injn_eq.
+    rewrite IHts1 by (simpl in *; omega).
+    rewrite cons_cons_eq.
+    tauto. }
+Qed.
+
+Local Lemma map_inj:
+  forall {A} (f : A -> A) xs,
+  map f xs = xs <->
+  Forall (fun x => f x = x) xs.
+Proof.
+  induction xs; simpl; intros; split; intros; eauto using Forall;
+  injections.
+  { econstructor; tauto. }
+  { pick Forall invert. f_equal; tauto. }
+Qed.
+
+Lemma fv_MMultiLet_0:
+  forall ts u k,
+  fv k (MMultiLet 0 ts u) <->
+  Forall (fv k) ts /\ fv (k + length ts) u.
+Proof.
+  intros. unfold fv.
+  autorewrite with subst.
+  rewrite MMultiLet_inj by eauto using map_length.
+  rewrite upn_upn, Nat.add_comm.
+  rewrite map_inj.
+  tauto.
+Qed.
+
+Lemma fv_MVars:
+  forall n,
+  Forall (fv n) (MVars n) <->
+  True.
+Proof.
+  split; [ eauto | intros _ ].
+  unfold MVars, nats.
+  eapply Forall_map.
+  eapply Forall_seq; intros.
+  fv. omega.
+Qed.
+
+Lemma fv_MProjs:
+  forall k n t,
+  fv k t -> (* not an equivalence, as [k] could be zero *)
+  Forall (fv k) (MProjs n t).
+Proof.
+  unfold MProjs. induction n; simpl; intros;
+  econstructor; [ rewrite fv_MProj |]; eauto.
+Qed.
+
+Hint Rewrite
+  fv_MTuple fv_MProj fv_MLetPair fv_MMultiLet_0
+  fv_MVars
+  (* not fv_MProjs *)
+: fv.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The following lemma is analogous to [fv_unaffected_regular], except it does
+   not have a regularity hypothesis, which makes it more pleasant to use. It is
+   proved by induction on terms, which is why we are unable to prove it in a
+   generic setting. *)
+
+Lemma fv_unaffected:
+  forall t k sigma,
+  fv k t ->
+  t.[upn k sigma] = t.
+Proof.
+  induction t; intros; fv; unpack; asimpl; repeat rewrite Nat.add_1_r in *;
+  try solve [ eauto using upn_k_sigma_x with typeclass_instances
+            | f_equal; eauto ].
+Qed.
+
+(* A corollary. *)
+
+Lemma closed_unaffected:
+  forall t sigma,
+  closed t ->
+  t.[sigma] = t.
+Proof.
+  unfold closed. intros.
+  rewrite <- (upn0 sigma).
+  eauto using fv_unaffected.
+Qed.
diff --git a/coq/MyList.v b/coq/MyList.v
new file mode 100644
index 0000000..f56127a
--- /dev/null
+++ b/coq/MyList.v
@@ -0,0 +1,125 @@
+Require Import List.
+Require Import MyTactics.
+
+(* A few random additions to the [List] module, which is woefully incomplete. *)
+
+(* -------------------------------------------------------------------------- *)
+
+Lemma rev_cons_app:
+  forall {A} (x : A) xs ys,
+  rev (x :: xs) ++ ys = rev xs ++ x :: ys.
+Proof.
+  intros. simpl. rewrite <- app_assoc. reflexivity.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+Lemma length_nil:
+  forall A,
+  length (@nil A) = 0.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma length_cons:
+  forall A (x : A) xs,
+  length (x :: xs) = 1 + length xs.
+Proof.
+  reflexivity.
+Qed.
+
+Hint Rewrite length_nil length_cons app_length map_length : length.
+
+Ltac length :=
+  autorewrite with length in *;
+  try omega.
+
+(* -------------------------------------------------------------------------- *)
+
+(* We have [app_nth1] and [app_nth2], but the following lemma, which can be
+   viewed as a special case of [app_nth2], is missing. *)
+
+Lemma app_nth:
+  forall {A} (xs ys : list A) x n,
+  n = length xs ->
+  nth n (xs ++ ys) x = nth 0 ys x.
+Proof.
+  intros.
+  rewrite app_nth2 by omega.
+  replace (n - length xs) with 0 by omega.
+  reflexivity.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [rev_nats n] is the semi-open interval (n, 0], counted down. *)
+
+(* It could also be defined as [rev (seq 0 n)], but a direct definition
+   is easier to work with, as it is immediately amenable to proofs by
+   induction. *)
+
+Fixpoint rev_nats (n : nat) : list nat :=
+  match n with
+  | 0 =>
+      nil
+  | S n =>
+      n :: rev_nats n
+  end.
+
+(* [nats n] is the semi-open interval [0, n), counted up. *)
+
+Definition nats (n : nat) : list nat :=
+  seq 0 n.
+
+(* These sequences have length [n]. *)
+
+Lemma length_rev_nats:
+  forall n,
+  length (rev_nats n) = n.
+Proof.
+  induction n; intros; simpl; [| rewrite IHn ]; eauto.
+Qed.
+
+Lemma length_nats:
+  forall n,
+  length (nats n) = n.
+Proof.
+  unfold nats. intros. eauto using seq_length.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A few basic lemmas about [Forall]. *)
+
+Lemma Forall_map:
+  forall A B (f : A -> B) (P : B -> Prop) xs,
+  Forall (fun x => P (f x)) xs ->
+  Forall P (map f xs).
+Proof.
+  induction 1; intros; subst; simpl; econstructor; eauto.
+Qed.
+
+Lemma Forall_app:
+  forall A (P : A -> Prop) xs ys,
+  Forall P xs ->
+  Forall P ys ->
+  Forall P (xs ++ ys).
+Proof.
+  induction 1; intros; subst; simpl; eauto.
+Qed.
+
+Lemma Forall_rev:
+  forall A (P : A -> Prop) xs,
+  Forall P xs ->
+  Forall P (rev xs).
+Proof.
+  induction 1; intros; subst; simpl; eauto using Forall_app.
+Qed.
+
+Lemma Forall_seq:
+  forall (P : nat -> Prop) len start,
+  (forall i, start <= i < start + len -> P i) ->
+  Forall P (seq start len).
+Proof.
+  induction len; intros; simpl; econstructor; eauto with omega.
+Qed.