diff --git a/coq/AutosubstExtra.v b/coq/AutosubstExtra.v
new file mode 100644
index 0000000..af2ad35
--- /dev/null
+++ b/coq/AutosubstExtra.v
@@ -0,0 +1,169 @@
+Require Import Omega.
+Require Import Autosubst.Autosubst.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A more recognizable notation for lifting. *)
+
+Notation lift i t := (t.[ren(+i)]).
+
+(* -------------------------------------------------------------------------- *)
+
+Section Extras.
+
+Context A `{Ids A, Rename A, Subst A, SubstLemmas A}.
+
+Lemma up_ren:
+  forall xi,
+  ren (upren xi) = up (ren xi).
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma upn_ren:
+  forall i xi,
+  ren (iterate upren i xi) = upn i (ren xi).
+Proof.
+  induction i; intros.
+  { reflexivity. }
+  { rewrite <- fold_up_upn. rewrite <- IHi. asimpl. reflexivity. }
+Qed.
+
+Lemma plus_upn: (* close to [up_liftn] *)
+  forall i sigma,
+  (+i) >>> upn i sigma = sigma >> ren (+i).
+Proof.
+  induction i; intros.
+  { rewrite iterate_0. autosubst. }
+  { rewrite iterate_S. asimpl. rewrite IHi. autosubst. }
+Qed.
+
+Lemma up_sigma_up_ren:
+  forall t i sigma,
+  t.[up sigma].[up (ren (+i))] = t.[up (ren (+i))].[upn (1 + i) sigma].
+Proof.
+  intros. asimpl. rewrite plus_upn. asimpl. reflexivity.
+Qed.
+
+Lemma upn_k_sigma_x:
+  forall k sigma x,
+  x < k ->
+  upn k sigma x = ids x.
+Proof.
+  induction k; intros; asimpl.
+  { omega. }
+  { destruct x; asimpl.
+    { eauto. }
+    { rewrite IHk by omega. autosubst. }
+  }
+Qed.
+
+Lemma push_substitution_last:
+  forall t v i,
+  t.[v .: ren (+i)] = t.[up (ren (+i))].[v/].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma push_substitution_last_up_hoist:
+  forall t v i j,
+  t.[up (v .: ren (+i))].[up (ren (+j))] =
+  t.[up (up (ren (+j + i)))].[up (lift j v .: ids)].
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma lift_lift:
+  forall i j t,
+  lift i (lift j t) = lift (i + j) t.
+Proof.
+  intros. autosubst.
+Qed.
+
+Lemma lift_upn:
+  forall t i sigma,
+  (lift i t).[upn i sigma] = lift i t.[sigma].
+Proof.
+  intros. asimpl.
+  erewrite plus_upn.
+  reflexivity.
+Qed.
+
+Lemma lift_up:
+  forall t sigma,
+  (lift 1 t).[up sigma] = lift 1 t.[sigma].
+Proof.
+  intros. change up with (upn 1). eapply lift_upn.
+Qed.
+
+Lemma up_sigma_f:
+  forall (sigma : var -> A) (f : A -> A),
+  f (ids 0) = ids 0 ->
+  (forall i t, lift i (f t) = f (lift i t)) ->
+  up (sigma >>> f) = up sigma >>> f.
+Proof.
+  intros. f_ext. intros [|x]; asimpl; eauto.
+Qed.
+
+Lemma upn_sigma_f:
+  forall (sigma : var -> A) (f : A -> A),
+  f (ids 0) = ids 0 ->
+  (forall i t, lift i (f t) = f (lift i t)) ->
+  forall i,
+  upn i (sigma >>> f) = upn i sigma >>> f.
+Proof.
+  induction i; intros.
+  { reflexivity. }
+  { do 2 rewrite <- fold_up_upn. rewrite IHi. erewrite up_sigma_f by eauto. reflexivity. }
+Qed.
+
+Lemma upn_theta_sigma_ids:
+  forall theta sigma i,
+  theta >> sigma = ids ->
+  upn i theta >> upn i sigma = ids.
+Proof.
+  intros theta sigma i Hid.
+  rewrite up_comp_n.
+  rewrite Hid.
+  rewrite up_id_n.
+  reflexivity.
+Qed.
+
+Lemma up_theta_sigma_ids:
+  forall theta sigma,
+  theta >> sigma = ids ->
+  up theta >> up sigma = ids.
+Proof.
+  change up with (upn 1). eauto using upn_theta_sigma_ids.
+Qed.
+
+Lemma scons_scomp:
+  forall (T : A) Gamma theta,
+  T.[theta] .: (Gamma >> theta) = (T .: Gamma) >> theta.
+Proof.
+  intros. autosubst.
+Qed.
+
+(* BUG: the two sides of this equation are distinct, yet they are
+   printed identically. *)
+
+Goal
+  forall v f,
+  v .: (ids >>> f) = (v .: ids) >>> f.
+Proof.
+  intros.
+  Fail reflexivity.
+Abort.
+
+End Extras.
+
+(* This incantation means that [eauto with autosubst] can use the tactic
+   [autosubst] to prove an equality. *)
+
+Hint Extern 1 (_ = _) => autosubst : autosubst.
+
+(* This incantation means that [eauto with autosubst] can use the lemmas
+   whose names are listed here. This is useful when an equality involves
+   metavariables, so the tactic [autosubst] fails. *)
+
+Hint Resolve scons_scomp : autosubst.
diff --git a/coq/Autosubst_IsRen.v b/coq/Autosubst_IsRen.v
new file mode 100644
index 0000000..152782b
--- /dev/null
+++ b/coq/Autosubst_IsRen.v
@@ -0,0 +1,87 @@
+Require Import Coq.Logic.ClassicalUniqueChoice.
+Require Import Autosubst.Autosubst.
+Require Import AutosubstExtra.
+
+Section Lemmas.
+
+Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
+
+(* The predicate [is_ren sigma] means that the substitution [sigma] is in fact
+   a renaming [ren xi]. *)
+
+(* When stating a lemma that involves a renaming, it is preferable to use a
+   substitution [sigma], together with a hypothesis [is_ren sigma], rather
+   than request that [sigma] be of the form [ren xi]. This allows us to use
+   [obvious] to check that [sigma] is a renaming, whereas we would otherwise
+   have to manually rewrite [sigma] to the form [ren xi]. *)
+
+Definition is_ren sigma :=
+  exists xi, sigma = ren xi.
+
+(* One way of proving that [sigma] is a renaming is to prove that [sigma] maps
+   every variable [x] to a variable [y]. *)
+
+Lemma prove_is_ren:
+  forall sigma,
+  (forall x y, ids x = ids y -> x = y) ->
+  (forall x, exists y, sigma x = ids y) ->
+  is_ren sigma.
+Proof.
+  (* This proof uses the axiom of unique choice. If one is willing to use
+     the stronger axiom of choice, then one can remove the hypothesis that
+     [ids] is injective. *)
+  intros ? Hinj Hxy.
+  assert (Hxi: exists xi : var -> var, forall x, sigma x = ids (xi x)).
+  { eapply unique_choice with (R := fun x y => sigma x = ids y).
+    intros x. destruct (Hxy x) as [ y Heqy ]. exists y.
+    split.
+    { assumption. }
+    { intros x' Heqx'. eapply Hinj. congruence. }
+  }
+  destruct Hxi as [ xi ? ].
+  exists xi.
+  f_ext; intros x. eauto.
+Qed.
+
+(* Applying [up] or [upn i] to a renaming produces a renaming. *)
+
+Lemma up_is_ren:
+  forall sigma,
+  is_ren sigma ->
+  is_ren (up sigma).
+Proof.
+  intros ? [ xi ? ]. subst. exists (upren xi).
+  erewrite <- up_ren by eauto with typeclass_instances. reflexivity.
+Qed.
+
+Lemma upn_is_ren:
+  forall sigma i,
+  is_ren sigma ->
+  is_ren (upn i sigma).
+Proof.
+  intros ? ? [ xi ? ]. subst. exists (iterate upren i xi).
+  erewrite <- upn_ren by eauto with typeclass_instances. reflexivity.
+Qed.
+
+(* Composing two renamings yields a renaming. *)
+
+Lemma comp_is_ren:
+  forall sigma1 sigma2,
+  is_ren sigma1 ->
+  is_ren sigma2 ->
+  is_ren (sigma1 >> sigma2).
+Proof.
+  intros ? ? [ xi1 ? ] [ xi2 ? ]. subst. exists (xi1 >>> xi2). autosubst.
+Qed.
+
+Lemma is_ren_ids:
+  is_ren ids.
+Proof.
+  exists id. autosubst.
+Qed.
+
+End Lemmas.
+
+Hint Unfold is_ren : is_ren obvious.
+
+Hint Resolve up_is_ren upn_is_ren comp_is_ren is_ren_ids : is_ren obvious.
diff --git a/coq/LambdaCalculusBigStep.v b/coq/LambdaCalculusBigStep.v
new file mode 100644
index 0000000..0e1c4c6
--- /dev/null
+++ b/coq/LambdaCalculusBigStep.v
@@ -0,0 +1,534 @@
+Require Import List.
+Require Import MyTactics.
+Require Import Sequences.
+Require Import LambdaCalculusSyntax.
+Require Import LambdaCalculusFreeVars.
+Require Import LambdaCalculusValues.
+Require Import LambdaCalculusReduction.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* A big-step call-by-value semantics. *)
+
+Inductive bigcbv : term -> term -> Prop :=
+| BigcbvValue:
+    forall v,
+    is_value v ->
+    bigcbv v v
+| BigcbvApp:
+    forall t1 t2 u1 v2 v,
+    bigcbv t1 (Lam u1) ->
+    bigcbv t2 v2 ->
+    bigcbv u1.[v2/] v ->
+    bigcbv (App t1 t2) v
+| BigcbvLet:
+    forall t1 t2 v1 v,
+    bigcbv t1 v1 ->
+    bigcbv t2.[v1/] v ->
+    bigcbv (Let t1 t2) v
+.
+
+Hint Constructors bigcbv : bigcbv.
+
+(* The tactic [invert_bigcbv] looks for a hypothesis of the form [bigcbv t v]
+   and inverts it. *)
+
+Ltac invert_bigcbv :=
+  pick bigcbv invert;
+  try solve [ false; eauto 3 with obvious ].
+
+(* -------------------------------------------------------------------------- *)
+
+(* If [bigcbv t v] holds, then [v] must be a value. *)
+
+Lemma bigcbv_is_value:
+  forall t v,
+  bigcbv t v ->
+  is_value v.
+Proof.
+  induction 1; eauto.
+Qed.
+
+Hint Resolve bigcbv_is_value : is_value obvious.
+
+(* -------------------------------------------------------------------------- *)
+
+(* If [t] evaluates to [v] according to the big-step semantics,
+   then [t] reduces to [v] according to the small-step semantics. *)
+
+Lemma bigcbv_star_cbv:
+  forall t v,
+  bigcbv t v ->
+  star cbv t v.
+Proof.
+  (* A detailed proof: *)
+  induction 1.
+  (* BigcbvValue *)
+  { eapply star_refl. }
+  (* BigcbvApp *)
+  { eapply star_trans. obvious.
+    eapply star_trans. obvious.
+    eapply star_step. obvious.
+    eauto. }
+  (* BigcbvLet *)
+  { eapply star_trans. obvious.
+    eapply star_step. obvious.
+    eauto. }
+Restart.
+  (* A much shorter proof: *)
+  induction 1; eauto 6 with sequences obvious.
+Qed.
+
+(* Conversely, if [t] reduces to [v] in the small-step semantics,
+   then [t] evaluates to [v] in the big-step semantics. *)
+
+Lemma cbv_bigcbv_bigcbv:
+  forall t1 t2,
+  cbv t1 t2 ->
+  forall v,
+  bigcbv t2 v ->
+  bigcbv t1 v.
+Proof.
+  (* A detailed proof: *)
+  induction 1; intros; subst; try solve [ false; tauto ].
+  (* BetaV *)
+  { econstructor; eauto with bigcbv. }
+  (* LetV *)
+  { econstructor; eauto with bigcbv. }
+  (* AppL *)
+  { invert_bigcbv. eauto with bigcbv. }
+  (* AppR *)
+  { invert_bigcbv. eauto with bigcbv. }
+  (* LetL *)
+  { invert_bigcbv. eauto with bigcbv. }
+Restart.
+  (* A shorter proof: *)
+  induction 1; intros; subst; try solve [ false; tauto
+  | econstructor; eauto with bigcbv
+  | invert_bigcbv; eauto with bigcbv
+  ].
+Qed.
+
+Lemma star_cbv_bigcbv:
+  forall t v,
+  star cbv t v ->
+  is_value v ->
+  bigcbv t v.
+Proof.
+  induction 1; eauto using cbv_bigcbv_bigcbv with bigcbv.
+Qed.
+
+(* In conclusion, we have the following equivalence: *)
+
+Theorem star_cbv_bigcbv_eq:
+  forall t v,
+  (star cbv t v /\ is_value v) <-> bigcbv t v.
+Proof.
+  split; intros; unpack;
+  eauto using star_cbv_bigcbv, bigcbv_star_cbv with is_value.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+(* A big-step call-by-value semantics with explicit environments. *)
+
+(* A closure is a pair of a term and an environment. A cvalue [cv] must be a
+   closure, as we have no other forms of values. An environment [e] is a list
+   of cvalues. *)
+
+(* We break the mutual induction between [cvalue] and [cenv] by inlining the
+   definition of [cenv] into the definition of [cvalue]. *)
+
+(* CVALUE *)
+Inductive cvalue :=
+| Clo: {bind term} -> list cvalue -> cvalue.
+
+Definition cenv :=
+  list cvalue.
+(* CVALUE *)
+
+(* This dummy cvalue is passed below as an argument to [nth], but is really
+   irrelevant, as the condition [x < length e] ensures that the dummy cvalue
+   is never used. *)
+
+Definition dummy_cvalue : cvalue :=
+  Clo (Var 0) nil.
+
+(* The judgement [ebigcbv e t cv] means that, under the environment [e], the
+   term [t] evaluates to [cv]. *)
+
+Inductive ebigcbv : cenv -> term -> cvalue -> Prop :=
+| EBigcbvVar:
+    forall e x cv,
+    (* The variable [x] must be in the domain of [e]. *)
+    x < length e ->
+    (* This allows us to safely look up [e] at [x]. *)
+    cv = nth x e dummy_cvalue ->
+    ebigcbv e (Var x) cv
+| EBigcbvLam:
+    forall e t,
+    (* The free variables of [t] must be less than or equal to [length e]. *)
+    (forall cv, fv (length (cv :: e)) t) ->
+    (* This allows us to build a closure that is indeed closed. *)
+    ebigcbv e (Lam t) (Clo t e)
+| EBigcbvApp:
+    forall e e' t1 t2 u1 cv2 cv,
+    (* Evaluate [t1] to a closure, *)
+    ebigcbv e t1 (Clo u1 e') ->
+    (* evaluate [t2] to a value, *)
+    ebigcbv e t2 cv2 ->
+    (* and evaluate the function body, in a suitable environment. *)
+    ebigcbv (cv2 :: e') u1 cv ->
+    ebigcbv e (App t1 t2) cv
+| EBigcbvLet:
+    forall e t1 t2 cv1 cv,
+    (* Evaluate [t1] to a value, *)
+    ebigcbv e t1 cv1 ->
+    (* and evaluate [t2] under a suitable environment. *)
+    ebigcbv (cv1 :: e) t2 cv ->
+    ebigcbv e (Let t1 t2) cv
+.
+
+Hint Constructors ebigcbv : ebigcbv.
+
+(* -------------------------------------------------------------------------- *)
+
+(* To explain what the above semantics means, and to prove that it is
+   equivalent to the big-step semantics, we first define a function that
+   decodes a cvalue into a value. *)
+
+(* Ideally, the function [decode] should be defined by the equation:
+
+     decode (Clo t e) = (Lam t).[decode_cenv e]
+
+   where the auxiliary function [decode_cenv] maps [decode] over the
+   environment [e], and converts the result to a substitution, that
+   is, a function of type [term -> term]:
+
+     decode_cenv e = fun x => nth x (map decode e) (decode dummy_cvalue)
+
+   The definitions below are a bit more awkward (as Coq does not support
+   mutual induction very well), but mean the same thing. *)
+
+Definition dummy_value : term :=
+  Lam (Var 0).
+
+Fixpoint decode (cv : cvalue) : term :=
+  match cv with
+  | Clo t e =>
+      (Lam t).[fun x => nth x (map decode e) dummy_value]
+  end.
+  (* I am not even sure why this definition is accepted by Coq? *)
+
+Definition decode_cenv e :=
+  fun x => nth x (map decode e) (decode dummy_cvalue).
+
+(* The first equation in the above comment is satisfied, as shown by
+   the following lemma. The second equation in the above comment is
+   satisfied too, by definition. *)
+
+Lemma decode_eq:
+  forall t e,
+  decode (Clo t e) = (Lam t).[decode_cenv e].
+Proof.
+  reflexivity.
+Qed.
+
+(* This equation is useful, too. *)
+
+Lemma decode_cenv_Var_eq:
+  forall x e,
+  (Var x).[decode_cenv e] = decode (nth x e dummy_cvalue).
+Proof.
+  intros. asimpl. unfold decode_cenv. rewrite map_nth. eauto.
+Qed.
+
+(* The tactic [decode] rewrites using the above two equations. *)
+
+Hint Rewrite decode_eq decode_cenv_Var_eq : decode.
+Ltac decode := autorewrite with decode in *.
+
+(* We make [decode] opaque, so its definition is not unfolded by Coq. *)
+
+Opaque decode.
+
+(* [decode cv] is always a value. *)
+
+Lemma is_value_decode:
+  forall cv,
+  is_value (decode cv).
+Proof.
+  intros. destruct cv. decode. asimpl. tauto.
+Qed.
+
+Lemma is_value_decode_cenv:
+  forall x e,
+  is_value (Var x).[decode_cenv e].
+Proof.
+  intros. decode. eauto using is_value_decode.
+Qed.
+
+Local Hint Resolve is_value_decode is_value_decode_cenv : is_value obvious.
+
+(* A composition of two substitutions is the same thing as one substitution. *)
+
+Lemma decode_cenv_cons:
+  forall t e cv,
+  t.[up (decode_cenv e)].[decode cv/] = t.[decode_cenv (cv :: e)].
+Proof.
+  intros. autosubst. (* wonderful *)
+Qed.
+
+(* The tactic [nonvalue_eq_decode] closes a subgoal when there is a hypothesis
+   of the form [_ = decode_cenv e x], where the left-hand side of the equation
+   clearly is not a value. This is a contradiction. *)
+
+Ltac nonvalue_eq_decode :=
+  match goal with
+  | heq: _ = decode_cenv ?e ?x |- _ =>
+      assert (hv: is_value (decode_cenv e x)); [
+        solve [ obvious ]
+      | rewrite <- heq in hv; false; is_value ]
+  end.
+
+(* -------------------------------------------------------------------------- *)
+
+(* If [t] evaluates to [cv] under environment [e],
+   then, in the big-step semantics,
+   the term [t.[decode_cenv e]] evaluates to the value [decode cv]. *)
+
+Lemma ebigcbv_bigcbv:
+  forall e t cv,
+  ebigcbv e t cv ->
+  bigcbv t.[decode_cenv e] (decode cv).
+Proof.
+  induction 1; intros; subst.
+  (* EBigcbvVar *)
+  { decode. econstructor. obvious. }
+  (* EBigcbvLam *)
+  { econstructor. obvious. }
+  (* EBigcbvApp *)
+  { decode.
+    asimpl. econstructor; eauto.
+    asimpl. eauto. }
+  (* EBigcbvLet *)
+  { asimpl. econstructor; eauto.
+    asimpl. eauto. }
+Qed.
+
+(* A simplified corollary, where [t] is closed and is therefore evaluated
+   under the empty environment. *)
+
+Lemma ebigcbv_bigcbv_nil:
+  forall t cv,
+  ebigcbv nil t cv ->
+  closed t ->
+  bigcbv t (decode cv).
+Proof.
+  intros.
+  replace t with t.[decode_cenv nil] by eauto using closed_unaffected.
+  eauto using ebigcbv_bigcbv.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The converse statement: if in the big-step semantics, the term
+   [t.[decode_cenv e]] evaluates to the value [decode cv], then [t] evaluates
+   to [cv] under environment [e]. *)
+
+(* This proof does not work (and, in fact, the statement is wrong). A failed
+   proof attempt reveals two problems... *)
+
+Lemma bigcbv_ebigcbv_failed:
+  forall e t cv,
+  bigcbv t.[decode_cenv e] (decode cv) ->
+  ebigcbv e t cv.
+Proof.
+  inversion 1; intros; subst.
+  (* BigcbvValue *)
+  { (* [t] must be a variable or a lambda-abstraction. *)
+    destruct t; [ | | false; is_value | false; is_value ].
+    (* Case: [t] is a variable. *)
+    { econstructor.
+      (* Here, we have two subgoals, neither of which can be proved. *)
+      { (* Problem 1: we are unable to prove [x < length e]. In order
+           to establish such a property, we would have to express the
+           hypothesis that the free variables of [t] are in the domain
+           of the environment [e]. And, for this hypothesis to be
+           inductive, we have to further require every closure in
+           the environment [e] to satisfy a similar condition. *)
+        admit. }
+      { (* Problem 2: we have [decode cv1 = decode cv2], and the goal
+           is [cv1 = cv2]. This goal cannot be proved, as the function
+           [decode] is not injective: multiple closures represent the
+           same lambda-abstraction. *)
+        decode.
+        admit. }
+Abort.
+
+(* -------------------------------------------------------------------------- *)
+
+(* In order to fix the above failed statement, we need to express the
+   following well-formedness invariant: whenever a closure [Clo t e] is
+   constructed, the free variables of the term [t] are in the domain of the
+   environment [env], and, recursively, every value in [e] is well-formed. *)
+
+Inductive wf_cvalue : cvalue -> Prop :=
+| WfCvalue:
+    forall t e,
+    (forall cv, fv (length (cv :: e)) t) ->
+    wf_cenv e ->
+    wf_cvalue (Clo t e)
+
+with wf_cenv : cenv -> Prop :=
+| WfCenv:
+    forall e,
+    Forall wf_cvalue e ->
+    wf_cenv e.
+
+(* The following trivial lemmas (which repeat the definition) are provided as
+   hints for [eauto with wf_cvalue]. *)
+
+Lemma use_wf_cvalue_1:
+  forall t e cv,
+  wf_cvalue (Clo t e) ->
+  fv (length (cv :: e)) t.
+Proof.
+  inversion 1; eauto.
+Qed.
+
+Lemma use_wf_cvalue_2:
+  forall t e,
+  wf_cvalue (Clo t e) ->
+  wf_cenv e.
+Proof.
+  inversion 1; eauto.
+Qed.
+
+Lemma prove_wf_cenv_nil:
+  wf_cenv nil.
+Proof.
+  econstructor. eauto.
+Qed.
+
+Lemma prove_wf_cenv_cons:
+  forall cv e,
+  wf_cvalue cv ->
+  wf_cenv e ->
+  wf_cenv (cv :: e).
+Proof.
+  inversion 2; intros; subst.
+  econstructor.
+  econstructor; eauto.
+Qed.
+
+Hint Resolve
+  use_wf_cvalue_1 use_wf_cvalue_2 prove_wf_cenv_nil prove_wf_cenv_cons
+: wf_cvalue.
+
+(* The following lemma states that the invariant is preserved by [ebigcbv].
+   That is, if the term [t] is successfully evaluated in the well-formed
+   environment [e] to a cvalue [cv], then [cv] is well-formed. *)
+
+Lemma ebigcbv_wf_cvalue:
+  forall e t cv,
+  ebigcbv e t cv ->
+  wf_cenv e ->
+  wf_cvalue cv.
+Proof.
+  induction 1; intros; subst.
+  (* EBigcbvVar *)
+  { pick wf_cenv invert. rewrite Forall_forall in *. eauto using nth_In. }
+  (* EBigcbvLam *)
+  { econstructor; eauto. }
+  (* EBigcbvApp *)
+  { eauto 6 with wf_cvalue. }
+  (* EBigcbvLet *)
+  { eauto 6 with wf_cvalue. }
+Qed.
+
+Hint Resolve ebigcbv_wf_cvalue : wf_cvalue.
+
+(* -------------------------------------------------------------------------- *)
+
+(* We can now make an amended statement: if in the big-step semantics, the
+   term [t.[decode_cenv e]] evaluates to a value [v], if the environment [e]
+   is well-formed, and if the free variables of [t] are in the domain of [e],
+   then under environment [e] the term [t] evaluates to some cvalue [cv] such
+   that [decode cv] is [v]. *)
+
+Lemma bigcbv_ebigcbv:
+  forall te v,
+  bigcbv te v ->
+  forall t e,
+  te = t.[decode_cenv e] ->
+  fv (length e) t ->
+  wf_cenv e ->
+  exists cv,
+  ebigcbv e t cv /\ decode cv = v.
+Proof.
+  induction 1; intros; subst.
+  (* BigcbvValue *)
+  { (* [t] must be a variable or a lambda-abstraction. *)
+    destruct t; [ | | false; is_value | false; is_value ]; fv.
+    (* Case: [t] is a variable. *)
+    { eexists; split. econstructor; eauto. decode. eauto. }
+    (* Case: [t] is a lambda-abstraction. *)
+    { eexists; split. econstructor; eauto. reflexivity. }
+  }
+  (* BigcbvApp *)
+  { (* [t] must be an application. *)
+    destruct t;
+    match goal with h: _ = _ |- _ => asimpl in h end;
+    [ nonvalue_eq_decode | false; congruence | | false; congruence ].
+    fv. unpack.
+    (* The equality [App _ _ = App _ _] can be simplified. *)
+    injections. subst.
+    (* Exploit two of the induction hypotheses (forward). *)
+    edestruct IHbigcbv1; eauto. unpack. clear IHbigcbv1.
+    edestruct IHbigcbv2; eauto. unpack. clear IHbigcbv2.
+    (* If [decode cv] is [Lam _], then [cv] must be a closure. This should
+       be a lemma. Because (here) every cvalue is a closure, it is trivial. *)
+    match goal with h: decode ?cv = Lam _ |- _ =>
+      destruct cv as [ t' e' ];
+      rewrite decode_eq in h;
+      asimpl in h;
+      injections; subst
+    end.
+    (* Now, exploit the third induction hypothesis (forward). *)
+    edestruct IHbigcbv3; eauto using decode_cenv_cons with wf_cvalue.
+    unpack. clear IHbigcbv3.
+    (* The result follows. *)
+    eauto with ebigcbv.
+  }
+  (* BigcbvLet *)
+  { (* [t] must be a [Let] construct. *)
+    destruct t;
+    match goal with h: _ = _ |- _ => asimpl in h end;
+    [ nonvalue_eq_decode | false; congruence | false; congruence | ].
+    fv. unpack.
+    injections. subst.
+    (* Exploit the induction hypotheses (forward). *)
+    edestruct IHbigcbv1; eauto. unpack. clear IHbigcbv1.
+    edestruct IHbigcbv2; eauto using decode_cenv_cons with wf_cvalue.
+    unpack. clear IHbigcbv2.
+    (* The result follows. *)
+    eauto with ebigcbv.
+  }
+Qed.
+
+(* A simplified corollary, where [t] is closed and is therefore evaluated
+   under the empty environment. *)
+
+Lemma bigcbv_ebigcbv_nil:
+  forall t v,
+  bigcbv t v ->
+  closed t ->
+  exists cv,
+  ebigcbv nil t cv /\ decode cv = v.
+Proof.
+  intros. eapply bigcbv_ebigcbv; eauto with wf_cvalue.
+  rewrite closed_unaffected by eauto. reflexivity.
+Qed.
diff --git a/coq/LambdaCalculusFreeVars.v b/coq/LambdaCalculusFreeVars.v
new file mode 100644
index 0000000..1d5fdbb
--- /dev/null
+++ b/coq/LambdaCalculusFreeVars.v
@@ -0,0 +1,152 @@
+Require Import MyTactics.
+Require Import LambdaCalculusSyntax.
+
+(* This technical lemma states that the renaming [lift 1] is injective. *)
+
+Lemma lift_inj_Var:
+  forall t x,
+  lift 1 t = Var (S x) <-> t = Var x.
+Proof.
+  split; intros.
+  { eauto using lift_inj. }
+  { subst. eauto. }
+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:
+  forall k x,
+  fv k (Var x) <-> x < k.
+Proof.
+  unfold fv. asimpl. induction k; intros.
+  (* Base case. *)
+  { asimpl. split; intros; false.
+    { unfold ids, Ids_term in *. injections. omega. }
+    { omega. }
+  }
+  (* Step. *)
+  { destruct x; asimpl.
+    { split; intros. { omega. } { reflexivity. } }
+    rewrite lift_inj_Var. rewrite IHk. omega. }
+Qed.
+
+Lemma fv_Lam_eq:
+  forall k t,
+  fv k (Lam t) <-> fv (S k) t.
+Proof.
+  unfold fv. intros. asimpl. split; intros.
+  { injections. eauto. }
+  { unpack. congruence. }
+Qed.
+
+Lemma fv_App_eq:
+  forall k t1 t2,
+  fv k (App t1 t2) <-> fv k t1 /\ fv k t2.
+Proof.
+  unfold fv. intros. asimpl. split; intros.
+  { injections. eauto. }
+  { unpack. congruence. }
+Qed.
+
+Lemma fv_Let_eq:
+  forall k t1 t2,
+  fv k (Let t1 t2) <-> fv k t1 /\ fv (S k) t2.
+Proof.
+  unfold fv. intros. asimpl. split; intros.
+  { injections. eauto. }
+  { unpack. congruence. }
+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]. *)
+
+Lemma closed_Var:
+  forall x,
+  ~ closed (Var x).
+Proof.
+  unfold closed; intros; fv. omega.
+Qed.
+
+Lemma closed_AppL:
+  forall t1 t2,
+  closed (App t1 t2) ->
+  closed t1.
+Proof.
+  unfold closed; intros; fv. tauto.
+Qed.
+
+Lemma closed_AppR:
+  forall t1 t2,
+  closed (App t1 t2) ->
+  closed t2.
+Proof.
+  unfold closed; intros; fv. tauto.
+Qed.
+
+Lemma closed_LetL:
+  forall t1 t2,
+  closed (Let t1 t2) ->
+  closed t1.
+Proof.
+  unfold closed; intros; fv. tauto.
+Qed.
+
+Hint Resolve closed_Var closed_AppL closed_AppR closed_LetL : closed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* If the free variables of the term [t] are below [k], then [t] is unaffected
+   by a substitution of the form [upn k sigma]. *)
+
+Lemma fv_unaffected:
+  forall t k sigma,
+  fv k t ->
+  t.[upn k sigma] = t.
+Proof.
+  induction t; intros; fv; unpack; asimpl;
+  try solve [ eauto using upn_k_sigma_x with typeclass_instances
+            | f_equal; eauto ].
+Qed.
+
+(* If the term [t] is closed, then [t] is unaffected by any substitution. *)
+
+Lemma closed_unaffected:
+  forall t sigma,
+  closed t ->
+  t.[sigma] = t.
+Proof.
+  intros. eapply fv_unaffected with (k := 0). eauto.
+Qed.
diff --git a/coq/LambdaCalculusInterpreter.v b/coq/LambdaCalculusInterpreter.v
new file mode 100644
index 0000000..5796683
--- /dev/null
+++ b/coq/LambdaCalculusInterpreter.v
@@ -0,0 +1,226 @@
+Require Import Option.
+Require Import List.
+Require Import MyTactics.
+Require Import LambdaCalculusSyntax.
+Require Import LambdaCalculusFreeVars.
+Require Import LambdaCalculusBigStep.
+
+(* We now wish to define an interpreter for the lambda-calculus. In other
+   words, whereas [ebigcbv] is a relation, we now wish to define a function
+   [interpret] whose graph is the relation [ebigcbv]. *)
+
+(* At the moment, our lambda-calculus is pure (every value is a function)
+   so the interpreter cannot encounter a runtime error. *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* We might naively wish to write the following code, which Coq rejects,
+   because this function is not obviously terminating. (Exercise: which
+   recursive call is the culprit?) Indeed, an interpreter for the untyped
+   lambda-calculus does not always terminate: there are lambda-terms whose
+   evaluation diverges. (Exercise: exhibit a term that reduces to itself
+   in one or more reduction steps. Prove in Coq that this is the case.) *)
+
+(* FAILINTERPRET *)
+Fail Fixpoint interpret (e : cenv) (t : term) : cvalue :=
+  match t with
+  | Var x =>
+      nth x e dummy_cvalue
+        (* dummy is used when x is out of range *)
+  | Lam t =>
+      Clo t e
+  | App t1 t2 =>
+      let cv1 := interpret e t1 in
+      let cv2 := interpret e t2 in
+      match cv1 with Clo u1 e' =>
+        interpret (cv2 :: e') u1
+      end
+(* FAILINTERPRET *)
+  | Let t1 t2 =>
+      let cv1 := interpret e t1 in
+      interpret (cv1 :: e) t2
+(* FAILINTERPRET *)
+  end.
+(* FAILINTERPRET *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* There are several potential solutions to the above problem. One solution
+   would be to write code in (some implementation of) the partiality monad.
+   (See Dagand's lectures.) The solution proposed here is to parameterize
+   the function [interpret] with a natural integer [n], which serves as an
+   amount of "fuel" (or "effort") that we are willing to invest before we
+   give up. Thus, termination becomes obvious. The downside is that the
+   interpreter can now fail (which means "not enough fuel"). Fortunately,
+   given enough fuel, every terminating term can be evaluated. *)
+
+(* For Coq to accept the following definition, the fuel [n] must decrease at
+   every recursive call. We might wish to be more precise and somehow explain
+   that [n] needs to decrease only at the third recursive call in the case of
+   [App]lications. That would require defining a lexicographic ordering on the
+   pair [n, t], arguing that this ordering is well-founded, and defining
+   [interpret] by well-founded recursion. This can be done in Coq but is more
+   complicated, so (here) not worth the trouble. *)
+
+(* FIXINTERPRET *)
+Fixpoint interpret (n : nat) e t : option cvalue :=
+  match n with
+  | 0   => None (* not enough fuel *)
+  | S n =>
+      match t with
+      | Var x     => Some (nth x e dummy_cvalue)
+      | Lam t     => Some (Clo t e)
+      | App t1 t2 =>
+          interpret n e t1 >>= fun cv1 =>
+          interpret n e t2 >>= fun cv2 =>
+          match cv1 with Clo u1 e' =>
+            interpret n (cv2 :: e') u1
+          end
+(* FIXINTERPRET *)
+      | Let t1 t2 =>
+          interpret n e t1 >>= fun cv1 =>
+          interpret n (cv1 :: e) t2
+(* FIXINTERPRET *)
+  end end.
+(* FIXINTERPRET *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* The interpreter is correct with respect to the big-step semantics. *)
+
+Lemma interpret_ebigcbv:
+  forall n e t cv,
+  interpret n e t = Some cv ->
+  fv (length e) t ->
+  wf_cenv e ->
+  ebigcbv e t cv.
+Proof.
+  (* The definition of [interpret] is by induction on [n], so this proof
+     must be by induction on [n] as well. *)
+  induction n; destruct t; simpl; intros;
+  fv; unpack; injections; subst;
+  try solve [ congruence ].
+  (* Var *)
+  { econstructor; eauto. }
+  (* Lam *)
+  { econstructor; eauto. }
+  (* App *)
+  { repeat invert_bind_Some.
+    (* Every cvalue is a closure. Name the components of the closure
+       obtained by interpreting [t1]. *)
+    match goal with h: interpret _ _ t1 = Some ?cv |- _ =>
+      destruct cv as [ t' e' ]
+    end.
+    (* The goal follows. *)
+    econstructor; eauto 11 with wf_cvalue. }
+  (* Let *)
+  { invert_bind_Some.
+    econstructor; eauto with wf_cvalue. }
+Qed.
+
+(* A simplified corollary, where [t] is closed and is therefore evaluated
+   under the empty environment, and where we conclude with a [bigcbv]
+   judgement. *)
+
+Lemma interpret_bigcbv_nil:
+  forall n t cv,
+  interpret n nil t = Some cv ->
+  closed t ->
+  bigcbv t (decode cv).
+Proof.
+  eauto using ebigcbv_bigcbv_nil, interpret_ebigcbv with wf_cvalue.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The interpreter is monotonic with respect to the amount of fuel that is
+   provided: the more fuel, the better (that is, the more defined the result). *)
+
+Lemma interpret_monotonic:
+  forall n1 n2 e t,
+  n1 <= n2 ->
+  less_defined (interpret n1 e t) (interpret n2 e t).
+Proof.
+  (* This series of tactics get rid of the easy cases: *)
+  induction n1; destruct t; simpl; intros;
+  (* [less_defined None _] is always true. *)
+  eauto with less_defined;
+  (* If [S n1 <= n2], then [n2] must be a successor. *)
+  (destruct n2; [ omega |]); simpl;
+  (* [less_defined] is reflexive. *)
+  eauto with less_defined.
+
+  (* Two more complex cases remain, namely [App] and [Let]. Probably
+     the proof could be further automated, but I did not try. *)
+  (* App *)
+  { eapply prove_less_defined_bind.
+    { eauto using le_S_n. }
+    { intros _ [ t' e' ]. (* destruct the closure produced by [t1] *)
+      eapply prove_less_defined_bind; eauto using le_S_n. }
+  }
+  (* Let *)
+  { eauto 6 using le_S_n with less_defined. }
+Qed.
+
+(* A reformulation. *)
+
+Lemma interpret_monotonic_corollary:
+  forall n1 n2 e t cv,
+  interpret n1 e t = Some cv ->
+  n1 <= n2 ->
+  interpret n2 e t = Some cv.
+Proof.
+  generalize interpret_monotonic. unfold less_defined. eauto.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The interpreter is complete with respect to the big-step semantics
+   [ebigcbv]. That is, given enough fuel, and given a term whose value is
+   [cv], it will compute [cv]. *)
+
+Lemma ebigcbv_interpret:
+  forall e t cv,
+  ebigcbv e t cv ->
+  exists n,
+  interpret n e t = Some cv.
+Proof.
+  (* We can see, in the proof, that the necessary amount of fuel, [n], is
+     the height of the derivation of the judgement [ebigcbv e t cv].
+     Indeed, at every [App] or [Let] node, we count 1 plus the maximum
+     amount of fuel required by our children. *)
+  induction 1; intros; subst.
+  (* EBigcbvVar *)
+  { exists 1. eauto. }
+  (* EBigcbvLam *)
+  { exists 1. eauto. }
+  (* EBigcbvApp *)
+  { destruct IHebigcbv1 as [ n1 ? ].
+    destruct IHebigcbv2 as [ n2 ? ].
+    destruct IHebigcbv3 as [ n3 ? ].
+    eexists (S (max (max n1 n2) n3)). simpl.
+    eauto 6 using prove_bind_Some, interpret_monotonic_corollary with omega. }
+  (* EBigcbvLet *)
+  { destruct IHebigcbv1 as [ n1 ? ].
+    destruct IHebigcbv2 as [ n2 ? ].
+    eexists (S (max n1 n2)). simpl.
+    eauto using prove_bind_Some, interpret_monotonic_corollary with omega. }
+Qed.
+
+(* The interpreter is complete with respect to the big-step semantics
+   [bigcbv]. That is, given enough fuel, and given a term [t] whose value is
+   [v], it will compute a cvalue [cv] which decodes to [v]. We state this in
+   the case where [t] is closed and is therefore evaluated under the empty
+   environment. *)
+
+Lemma bigcbv_interpret_nil:
+  forall t v,
+  bigcbv t v ->
+  closed t ->
+  exists n cv,
+  interpret n nil t = Some cv /\ decode cv = v.
+Proof.
+  intros.
+  edestruct bigcbv_ebigcbv_nil; eauto. unpack.
+  edestruct ebigcbv_interpret; eauto.
+Qed.
diff --git a/coq/LambdaCalculusReduction.v b/coq/LambdaCalculusReduction.v
new file mode 100644
index 0000000..0830f95
--- /dev/null
+++ b/coq/LambdaCalculusReduction.v
@@ -0,0 +1,619 @@
+Require Import MyTactics.
+Require Import Sequences.
+Require Import LambdaCalculusSyntax.
+Require Import LambdaCalculusValues.
+Require Import LambdaCalculusFreeVars.
+
+(* We give a symbolic name to each reduction rule. *)
+
+Inductive rule :=
+| RuleBetaV    (* reduction of a beta-v redex: (\x.t) v                   *)
+| RuleLetV     (* reduction of a let-v redex:  let x = v in t             *)
+| RuleBeta     (* reduction of a beta   redex: (\x.t) u                   *)
+| RuleLet      (* reduction of a let redex:    let x = u in t             *)
+| RuleParBetaV (* reduction of a beta-v redex and reduction in both sides *)
+| RuleParLetV  (* reduction of a let redex and reduction in both sides    *)
+| RuleVar      (* no reduction                                            *)
+| RuleLam      (* reduction in [Lam _]                                    *)
+| RuleAppL     (* reduction in [App _ u]                                  *)
+| RuleAppVR    (* reduction in [App v _], if [v] is a value               *)
+| RuleAppLR    (* reduction in both sides of [App _ _]                    *)
+| RuleLetL     (* reduction in [Let _ u]                                  *)
+| RuleLetR     (* reduction in [Let t _]                                  *)
+| RuleLetLR    (* reduction in both sides of [Let _ _]                    *).
+
+(* A mask is a set of rules. *)
+
+Definition mask :=
+  rule -> Prop.
+
+(* A generic small-step reduction semantics, parameterized with a mask. *)
+
+Inductive red (mask : mask) : term -> term -> Prop :=
+| RedBetaV:
+    forall t v u,
+    mask RuleBetaV ->
+    is_value v ->
+    t.[v/] = u ->
+    red mask (App (Lam t) v) u
+| RedLetV:
+    forall t v u,
+    mask RuleLetV ->
+    is_value v ->
+    t.[v/] = u ->
+    red mask (Let v t) u
+| RedBeta:
+    forall t1 t2 u,
+    mask RuleBeta ->
+    t1.[t2/] = u ->
+    red mask (App (Lam t1) t2) u
+| RedLet:
+    forall t1 t2 u,
+    mask RuleLet ->
+    t2.[t1/] = u ->
+    red mask (Let t1 t2) u
+| RedParBetaV:
+    forall t1 v1 t2 v2 u,
+    mask RuleParBetaV ->
+    is_value v1 ->
+    red mask t1 t2 ->
+    red mask v1 v2 ->
+    t2.[v2/] = u ->
+    red mask (App (Lam t1) v1) u
+| RedParLetV:
+    forall t1 t2 v1 v2 u,
+    mask RuleParLetV ->
+    is_value v1 ->
+    red mask t1 t2 ->
+    red mask v1 v2 ->
+    t2.[v2/] = u ->
+    red mask (Let v1 t1) u
+| RedVar:
+    forall x,
+    mask RuleVar ->
+    red mask (Var x) (Var x)
+| RedLam:
+    forall t1 t2,
+    mask RuleLam ->
+    red mask t1 t2 ->
+    red mask (Lam t1) (Lam t2)
+| RedAppL:
+    forall t1 t2 u,
+    mask RuleAppL ->
+    red mask t1 t2 ->
+    red mask (App t1 u) (App t2 u)
+| RedAppVR:
+    forall v u1 u2,
+    mask RuleAppVR ->
+    is_value v ->
+    red mask u1 u2 ->
+    red mask (App v u1) (App v u2)
+| RedAppLR:
+    forall t1 t2 u1 u2,
+    mask RuleAppLR ->
+    red mask t1 t2 ->
+    red mask u1 u2 ->
+    red mask (App t1 u1) (App t2 u2)
+| RedLetL:
+    forall t1 t2 u,
+    mask RuleLetL ->
+    red mask t1 t2 ->
+    red mask (Let t1 u) (Let t2 u)
+| RedLetR:
+    forall t u1 u2,
+    mask RuleLetR ->
+    red mask u1 u2 ->
+    red mask (Let t u1) (Let t u2)
+| RedLetLR:
+    forall t1 t2 u1 u2,
+    mask RuleLetLR ->
+    red mask t1 t2 ->
+    red mask u1 u2 ->
+    red mask (Let t1 u1) (Let t2 u2)
+.
+
+Hint Constructors red : red obvious.
+
+(* The following mask defines the call-by-value reduction semantics. *)
+
+Definition cbv_mask rule :=
+  match rule with
+  | RuleBetaV    (* reduction of a beta-v redex: (\x.t) v                 *)
+  | RuleLetV     (* reduction of a let-v redex:  let x = v in t           *)
+  | RuleAppL     (* reduction in [App _ u]                                *)
+  | RuleAppVR    (* reduction in [App v _], if [v] is a value             *)
+  | RuleLetL     (* reduction in [Let _ u]                                *)
+      => True
+  | _ => False
+  end.
+
+Notation cbv := (red cbv_mask).
+
+(* The following mask defines the call-by-name reduction semantics. *)
+
+Definition cbn_mask rule :=
+  match rule with
+  | RuleBeta     (* reduction of a beta   redex: (\x.t) v                 *)
+  | RuleLet      (* reduction of a let redex:    let x = v in t           *)
+  | RuleAppL     (* reduction in [App _ u]                                *)
+      => True
+  | _ => False
+  end.
+
+Notation cbn := (red cbn_mask).
+
+(* The parallel by-value reduction semantics allows beta-v reductions under
+   arbitrary contexts, including under lambda-abstractions. Furthermore, it
+   allows parallel reductions (and allows no reduction at all). *)
+
+Definition pcbv_mask rule :=
+  match rule with
+  | RuleParBetaV (* reduction of a beta redex and reduction in both sides *)
+  | RuleParLetV  (* reduction of a let redex and reduction in both sides  *)
+  | RuleVar      (* no reduction                                          *)
+  | RuleLam      (* reduction in [Lam _]                                  *)
+  | RuleAppLR    (* reduction in both sides of [App _ _]                  *)
+  | RuleLetLR    (* reduction in both sides of [Let _ _]                  *)
+      => True
+  | _ => False
+  end.
+
+Notation pcbv := (red pcbv_mask).
+
+(* The tactic [obvious] should be able to prove goals of the form
+   [red mask t1 t2], where [mask] is a known mask. *)
+
+Hint Extern 1 (cbv_mask _)  => (simpl; tauto) : red obvious.
+Hint Extern 1 (cbn_mask _)  => (simpl; tauto) : red obvious.
+Hint Extern 1 (pcbv_mask _) => (simpl; tauto) : red obvious.
+
+Goal cbv (Let (App (Lam (Var 0)) (Var 0)) (Var 0)) (Let (Var 0) (Var 0)).
+Proof. obvious. Qed.
+
+Goal cbv (Let (Var 0) (Var 0)) (Var 0).
+Proof. obvious. Qed.
+
+Goal cbn (Let (Var 0) (Var 0)) (Var 0).
+Proof. obvious. Qed.
+
+Goal
+  let id := Lam (Var 0) in
+  let t := (Let (Lam (Var 0)) (Var 0)) in
+  cbn (App id t) t.
+Proof. simpl. obvious. Qed.
+
+Goal pcbv (App (App (Lam (Var 0)) (Var 0)) (App (Lam (Var 0)) (Var 0)))
+          (App (Var 0) (Var 0)).
+Proof.
+  eauto 8 with obvious.
+Qed.
+
+(* The tactic [step] applies to a goal of the form [star (red mask) t1 t2]. It
+   causes the term [t1] to take one step of reduction towards [t1'], turning
+   the goal into [star (red mask) t1' t2]. *)
+
+Ltac step :=
+  eapply star_step; [ obvious |].
+
+(* The tactic [finished] applies to a goal of the form [star (red mask) t1 t2].
+   It turns the goal into [t1 = t2]. *)
+
+Ltac finished :=
+  eapply star_refl_eq.
+
+(* The tactic [invert_cbv] inverts a hypothesis of the form [cbv t1 t2]. *)
+
+Ltac invert_cbv :=
+  pick (red cbv_mask) invert;
+  try solve [ false; eauto 3 with obvious ].
+
+Ltac invert_star_cbv :=
+  pick (star cbv) invert.
+
+Ltac invert_cbn :=
+  pick (red cbn_mask) invert;
+  try solve [ false; eauto 3 with obvious ].
+
+(* If the following four rules are enabled, then reduction is reflexive. *)
+
+Lemma red_refl:
+  forall mask : mask,
+  mask RuleVar ->
+  mask RuleLam ->
+  mask RuleAppLR ->
+  mask RuleLetLR ->
+  forall t,
+  red mask t t.
+Proof.
+  induction t; eauto with red.
+Qed.
+
+(* [RuleBetaV] and [RuleLetV] are special cases of [RuleParBetaV] and
+   [RuleParLetV], hence are admissible in parallel call-by-value reduction. *)
+
+Lemma pcbv_RedBetaV:
+  forall t v u,
+  is_value v ->
+  t.[v/] = u ->
+  pcbv (App (Lam t) v) u.
+Proof.
+  eauto using red_refl with obvious.
+Qed.
+
+Lemma pcbv_RedLetV:
+  forall t v u,
+  is_value v ->
+  t.[v/] = u ->
+  pcbv (Let v t) u.
+Proof.
+  eauto using red_refl with obvious.
+Qed.
+
+(* Sequences of reduction, [star cbv], can be carried out under a context. *)
+
+Lemma star_cbv_AppL:
+  forall t1 t2 u,
+  star cbv t1 t2 ->
+  star cbv (App t1 u) (App t2 u).
+Proof.
+  induction 1; eauto with sequences obvious.
+Qed.
+
+Lemma star_pcbv_AppL:
+  forall t1 t2 u,
+  star pcbv t1 t2 ->
+  star pcbv (App t1 u) (App t2 u).
+Proof.
+  induction 1; eauto using red_refl with sequences obvious.
+Qed.
+
+Lemma plus_pcbv_AppL:
+  forall t1 t2 u,
+  plus pcbv t1 t2 ->
+  plus pcbv (App t1 u) (App t2 u).
+Proof.
+  induction 1.
+  econstructor; [ | eauto using star_pcbv_AppL ].
+  eapply RedAppLR; eauto using red_refl with obvious.
+Qed.
+
+Lemma star_cbv_AppR:
+  forall t u1 u2,
+  is_value t ->
+  star cbv u1 u2 ->
+  star cbv (App t u1) (App t u2).
+Proof.
+  induction 2; eauto with sequences obvious.
+Qed.
+
+Hint Resolve star_cbv_AppL star_pcbv_AppL plus_pcbv_AppL star_cbv_AppR : red obvious.
+
+Lemma star_cbv_AppLR:
+  forall t1 t2 u1 u2,
+  star cbv t1 t2 ->
+  star cbv u1 u2 ->
+  is_value t2 ->
+  star cbv (App t1 u1) (App t2 u2).
+Proof.
+  eauto with sequences obvious.
+Qed.
+
+Lemma star_cbv_LetL:
+  forall t1 t2 u,
+  star cbv t1 t2 ->
+  star cbv (Let t1 u) (Let t2 u).
+Proof.
+  induction 1; eauto with sequences obvious.
+Qed.
+
+Hint Resolve star_cbv_AppLR star_cbv_LetL : red obvious.
+
+(* Reduction commutes with substitutions of values for variables. (This
+   includes renamings.) This is true of every reduction strategy, with
+   the proviso that if [RuleVar] is enabled, then [RuleLam], [RuleAppLR]
+   and [RuleLetLR] must be enabled as well, so that reduction is reflexive. *)
+
+Lemma red_subst:
+  forall mask : mask,
+  (mask RuleVar -> mask RuleLam) ->
+  (mask RuleVar -> mask RuleAppLR) ->
+  (mask RuleVar -> mask RuleLetLR) ->
+  forall t1 t2,
+  red mask t1 t2 ->
+  forall sigma,
+  is_value_subst sigma ->
+  red mask t1.[sigma] t2.[sigma].
+Proof.
+  induction 4; simpl; intros; subst;
+  try solve [ econstructor; solve [ eauto with is_value | autosubst ]].
+  (* Case: [Var] *)
+  { eauto using red_refl. }
+Qed.
+
+Lemma star_red_subst:
+  forall mask : mask,
+  (mask RuleVar -> mask RuleLam) ->
+  (mask RuleVar -> mask RuleAppLR) ->
+  (mask RuleVar -> mask RuleLetLR) ->
+  forall t1 t2 sigma,
+  star (red mask) t1 t2 ->
+  is_value_subst sigma ->
+  star (red mask) t1.[sigma] t2.[sigma].
+Proof.
+  induction 4; eauto using red_subst with sequences.
+Qed.
+
+(* Call-by-value reduction is contained in parallel call-by-value. *)
+
+Lemma cbv_subset_pcbv:
+  forall t1 t2,
+  cbv t1 t2 ->
+  pcbv t1 t2.
+Proof.
+  induction 1; try solve [ tauto ]; eauto using red_refl with red.
+Qed.
+
+(* Under call-by-value, values do not reduce. *)
+
+Lemma values_do_not_reduce:
+  forall t1 t2,
+  cbv t1 t2 ->
+  ~ is_value t1.
+Proof.
+  inversion 1; is_value.
+Qed.
+
+Hint Resolve values_do_not_reduce : is_value obvious.
+
+Hint Extern 1 (False) => (eapply values_do_not_reduce) : is_value obvious.
+
+Lemma is_value_irred:
+  forall v,
+  is_value v ->
+  irred cbv v.
+Proof.
+  intros. intro. obvious.
+Qed.
+
+Hint Resolve is_value_irred : irred obvious.
+
+(* Under every strategy, the property of being a value is preserved by
+   reduction. *)
+
+Lemma values_are_stable:
+  forall mask v1 v2,
+  red mask v1 v2 ->
+  is_value v1 ->
+  is_value v2.
+Proof.
+  induction 1; is_value.
+Qed.
+
+Lemma nonvalues_are_stable:
+  forall mask v1 v2,
+  red mask v1 v2 ->
+  ~ is_value v2 ->
+  ~ is_value v1.
+Proof.
+  induction 1; is_value.
+Qed.
+
+Hint Resolve values_are_stable nonvalues_are_stable : is_value obvious.
+
+(* [cbv] is deterministic. *)
+
+Lemma cbv_deterministic:
+  forall t t1,
+  cbv t t1 ->
+  forall t2,
+  cbv t t2 ->
+  t1 = t2.
+Proof.
+  (* Induction over [cbv t t1]. *)
+  induction 1; try solve [ tauto ]; intros; subst;
+  (* Invert the second hypothesis, [cbv t t2]. The fact that values do not
+     reduce is used to eliminate some cases. *)
+  invert_cbv;
+  (* The result follows. *)
+  f_equal; eauto.
+Qed.
+
+(* Inversion lemmas for [irred]. *)
+
+Lemma invert_irred_cbv_App_1:
+  forall t u,
+  irred cbv (App t u) ->
+  irred cbv t.
+Proof.
+  intros. eapply irred_irred; obvious.
+Qed.
+
+Lemma invert_irred_cbv_App_2:
+  forall t u,
+  irred cbv (App t u) ->
+  is_value t ->
+  irred cbv u.
+Proof.
+  intros. eapply irred_irred; obvious.
+Qed.
+
+Lemma invert_irred_cbv_App_3:
+  forall t u,
+  irred cbv (App t u) ->
+  is_value t ->
+  is_value u ->
+  forall t', t <> Lam t'.
+Proof.
+  intros ? ? Hirred. repeat intro. subst.
+  eapply Hirred. obvious.
+Qed.
+
+Lemma invert_irred_cbv_Let_1:
+  forall t u,
+  irred cbv (Let t u) ->
+  irred cbv t.
+Proof.
+  intros. eapply irred_irred; obvious.
+Qed.
+
+Lemma invert_irred_cbv_Let_2:
+  forall t u,
+  irred cbv (Let t u) ->
+  ~ is_value t.
+Proof.
+  intros ? ? Hirred ?. eapply Hirred. obvious.
+Qed.
+
+Hint Resolve
+  invert_irred_cbv_App_1
+  invert_irred_cbv_App_2
+  invert_irred_cbv_Let_1
+  invert_irred_cbv_Let_2
+: irred.
+
+(* An analysis of irreducible terms for call-by-value reduction. A stuck
+   term is either an application [v1 v2] where [v1] is not a function or
+   a stuck term in an evaluation context. *)
+
+Inductive stuck : term -> Prop :=
+| StuckApp:
+    forall v1 v2,
+    is_value v1 ->
+    is_value v2 ->
+    (forall t, v1 <> Lam t) ->
+    stuck (App v1 v2)
+| StuckAppL:
+    forall t u,
+    stuck t ->
+    stuck (App t u)
+| StuckAppR:
+    forall v u,
+    is_value v ->
+    stuck u ->
+    stuck (App v u)
+| StuckLetL:
+    forall t u,
+    stuck t ->
+    stuck (Let t u).
+
+Hint Constructors stuck : stuck.
+
+(* To go wrong is to reduce to a stuck term. *)
+
+Definition goes_wrong t :=
+  exists t', star cbv t t' /\ stuck t'.
+
+(* A stuck term cannot be a value. *)
+
+Lemma stuck_nonvalue:
+  forall t,
+  stuck t ->
+  ~ is_value t.
+Proof.
+  induction 1; is_value.
+Qed.
+
+(* Every stuck term is irreducible. *)
+
+Ltac prove_irred_cbv :=
+  do 2 intro; invert_cbv.
+
+Lemma stuck_irred:
+  forall t,
+  stuck t ->
+  irred cbv t.
+Proof.
+  induction 1; prove_irred_cbv; try solve [
+    eauto using irreducible_terms_do_not_reduce
+  | eapply stuck_nonvalue; obvious
+  ].
+  (* StuckApp *)
+  { congruence. }
+Qed.
+
+Hint Resolve stuck_irred : irred obvious.
+
+(* Every irreducible term either is a value or is stuck. *)
+
+Lemma irred_cbv_is_value_or_stuck:
+  forall t,
+  irred cbv t ->
+  is_value t \/ stuck t.
+Proof.
+  induction t; intro Hirred;
+  try solve [ is_value ]; right.
+  (* App *)
+  { assert (H1: irred cbv t1). { eauto with irred. }
+    destruct (IHt1 H1); [| eauto with stuck ].
+    assert (H2: irred cbv t2). { eauto with irred. }
+    destruct (IHt2 H2); [| eauto with stuck ].
+    eapply StuckApp; eauto using invert_irred_cbv_App_3. }
+  (* Let *)
+  { assert (H: irred cbv t). { eauto with irred. }
+    destruct (IHt H); [| eauto with stuck ].
+    assert (~ is_value t). { eauto with irred. }
+    tauto. }
+Qed.
+
+(* The converse is true as well. *)
+
+Lemma irred_cbv_characterization:
+  forall t,
+  irred cbv t <->
+  is_value t \/ stuck t.
+Proof.
+  split.
+  { eauto using irred_cbv_is_value_or_stuck. }
+  { intuition eauto with irred. }
+Qed.
+
+(* A closed value must be a lambda-abstraction. *)
+
+Lemma closed_value:
+  forall v,
+  is_value v ->
+  closed v ->
+  exists t, v = Lam t.
+Proof.
+  intros. destruct v as [| t | | ]; try solve [ false; is_value ].
+  { false. eapply closed_Var. eauto. }
+  { exists t. eauto. }
+Qed.
+
+(* A stuck term cannot be closed. *)
+
+Lemma stuck_closed:
+  forall t,
+  stuck t ->
+  closed t ->
+  False.
+Proof.
+  induction 1; intros; eauto with closed.
+  (* StuckApp *)
+  { assert (ht1: exists t1, v1 = Lam t1).
+    { eauto using closed_value with closed. }
+    destruct ht1 as (?&?). subst v1. congruence. }
+Qed.
+
+(* Under call-by-value, every closed term either reduces or is a value. *)
+
+Lemma cbv_progress:
+  forall t,
+  closed t ->
+  is_value t \/ exists u, cbv t u.
+Local Ltac ih IH :=
+  destruct IH as [| [ ? ? ]]; [ eauto with closed | | obvious ].
+Proof.
+  (* We give a direct proof, but the result also follows from
+     [irred_cbv_is_value_or_stuck] and [stuck_closed]. *)
+  induction t as [| | t1 IHt1 t2 IHt2 | t1 IHt1 t2 IHt2 ];
+  try solve [ left; obvious ]; right.
+  (* App *)
+  { ih IHt1.
+    ih IHt2.
+    destruct (closed_value t1) as [ u1 ? ]; eauto with closed; subst t1.
+    obvious.
+  }
+  (* Let *)
+  { ih IHt1. obvious. }
+Qed.
diff --git a/coq/LambdaCalculusSyntax.v b/coq/LambdaCalculusSyntax.v
new file mode 100644
index 0000000..56d1898
--- /dev/null
+++ b/coq/LambdaCalculusSyntax.v
@@ -0,0 +1,192 @@
+Require Import Coq.Wellfounded.Inverse_Image.
+Require Import MyTactics.
+Require Export Autosubst.Autosubst.
+Require Export AutosubstExtra.
+Require Export Autosubst_IsRen.
+
+(* The syntax of the lambda-calculus. *)
+
+Inductive term :=
+| Var (x : var)
+| Lam (t : {bind term})
+| App (t1 t2 : term)
+| Let (t1 : term) (t2 : {bind term})
+.
+
+Instance Ids_term : Ids term. derive. Defined.
+Instance Rename_term : Rename term. derive. Defined.
+Instance Subst_term : Subst term. derive. Defined.
+Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+
+(* If the image of [t] through a substitution is a variable, then [t] must
+   itself be a variable. *)
+
+Lemma subst_is_var:
+  forall t sigma x,
+  t.[sigma] = ids x ->
+  exists y,
+  t = ids y.
+Proof.
+  intros ? ? ? Heq. destruct t; compute in Heq; solve [ eauto | congruence ].
+Qed.
+
+(* The identity substitution [ids] is injective. *)
+
+Lemma inj_ids:
+  forall x y,
+  ids x = ids y ->
+  x = y.
+Proof.
+  intros ? ? Heq. compute in Heq. congruence.
+Qed.
+
+(* If the composition of two substitutions [sigma1] and [sigma2] is the
+   identity substitution, then [sigma1] must be a renaming. *)
+
+Lemma ids_implies_is_ren:
+  forall sigma1 sigma2,
+  sigma1 >> sigma2 = ids ->
+  is_ren sigma1.
+Proof.
+  intros ? ? Hid.
+  eapply prove_is_ren; [ eapply inj_ids | intros x ].
+  eapply subst_is_var with (sigma := sigma2) (x := x).
+  rewrite <- Hid. reflexivity.
+Qed.
+
+Hint Resolve ids_implies_is_ren : is_ren obvious.
+
+(* The size of a term. *)
+
+Fixpoint size (t : term) : nat :=
+  match t with
+  | Var _ => 0
+  | Lam t => 1 + size t
+  | App t1 t2
+  | Let t1 t2 => 1 + size t1 + size t2
+  end.
+
+(* The size of a term is preserved by renaming. *)
+
+Lemma size_renaming:
+  forall t sigma,
+  is_ren sigma ->
+  size t.[sigma] = size t.
+Proof.
+  induction t; intros sigma Hsigma; asimpl;
+  repeat (match goal with h: forall sigma, _ |- _ => rewrite h by obvious; clear h end);
+  try reflexivity.
+  (* [Var] *)
+  { destruct Hsigma as [ xi ? ]. subst. reflexivity. }
+Qed.
+
+(* The [size] function imposes a well-founded ordering on terms. *)
+
+Lemma smaller_wf:
+  well_founded (fun t1 t2 => size t1 < size t2).
+Proof.
+  eauto using wf_inverse_image, lt_wf.
+Qed.
+
+(* The tactic [size_induction] facilitates proofs by induction on the
+   size of a term. The following lemmas are used in the construction
+   of this tactic. *)
+
+Lemma size_induction_intro:
+  forall (P : term -> Prop),
+  (forall n t, size t < n -> P t) ->
+  (forall t, P t).
+Proof.
+  eauto. (* just instantiate [n] with [size t + 1] *)
+Defined.
+
+Lemma size_induction_induction:
+  forall (P : term -> Prop),
+  (forall n, (forall t, size t < n -> P t) -> (forall t, size t < S n -> P t)) ->
+  (forall n t, size t < n -> P t).
+Proof.
+  intros P IH. induction n; intros.
+  { false. eapply Nat.nlt_0_r. eauto. }
+  { eauto. }
+Defined.
+
+Lemma size_induction:
+  forall (P : term -> Prop),
+  (forall n, (forall t, size t < n -> P t) -> (forall t, size t < S n -> P t)) ->
+  (forall t, P t).
+Proof.
+  intros P IH.
+  eapply size_induction_intro.
+  eapply size_induction_induction.
+  eauto.
+Defined.
+
+Ltac size_induction :=
+  (* We assume the goal is of the form [forall t, P t]. *)
+  intro t; pattern t;
+  match goal with |- ?P t =>
+    simpl; eapply (@size_induction P); clear
+  end;
+  intros n IH t Htn.
+  (* The goal should now be of the form [P t]
+     with a hypothesis [IH: (forall t, size t < n -> P t]
+     and a hypothesis [Htn: size t < S n]. *)
+
+(* The tactic [size] proves goals of the form [size t < n]. The tactic
+   [obvious] is also extended to prove such goals. *)
+
+Hint Extern 1 (size ?t.[?sigma] < ?n) =>
+  rewrite size_renaming by obvious
+  : size obvious.
+
+Hint Extern 1 (size ?t < ?n) =>
+  simpl in *; omega
+  : size obvious.
+
+Ltac size :=
+  eauto with size.
+
+(* The following is a direct proof of [smaller_wf]. We do not use any
+   preexisting lemmas, and end the proof with [Defined] instead of [Qed],
+   so as to make the proof term transparent. Also, we avoid the tactic
+   [omega], which produces huge proof terms. This allows Coq to compute
+   with functions that are defined by well-founded recursion. *)
+
+Lemma smaller_wf_transparent:
+  well_founded (fun t1 t2 => size t1 < size t2).
+Proof.
+  unfold well_founded. size_induction.
+  constructor; intros u Hu.
+  eapply IH. eapply lt_S_n. eapply le_lt_trans; eauto.
+Defined.
+
+(* The following lemmas can be useful in situations where the tactic
+   [asimpl] performs too much simplification. *)
+
+Lemma subst_var:
+  forall x sigma,
+  (Var x).[sigma] = sigma x.
+Proof.
+  autosubst.
+Qed.
+
+Lemma subst_lam:
+  forall t sigma,
+  (Lam t).[sigma] = Lam (t.[up sigma]).
+Proof.
+  autosubst.
+Qed.
+
+Lemma subst_app:
+  forall t1 t2 sigma,
+  (App t1 t2).[sigma] = App t1.[sigma] t2.[sigma].
+Proof.
+  autosubst.
+Qed.
+
+Lemma subst_let:
+  forall t1 t2 sigma,
+  (Let t1 t2).[sigma] = Let t1.[sigma] t2.[up sigma].
+Proof.
+  autosubst.
+Qed.
diff --git a/coq/LambdaCalculusValues.v b/coq/LambdaCalculusValues.v
new file mode 100644
index 0000000..dc6f8dd
--- /dev/null
+++ b/coq/LambdaCalculusValues.v
@@ -0,0 +1,179 @@
+Require Import MyTactics.
+Require Import LambdaCalculusSyntax.
+
+(* The syntactic subcategory of values is decidable. *)
+
+Definition if_value {A} (t : term) (a1 a2 : A) : A :=
+  match t with
+  | Var _ | Lam _ => a1
+  | _ => a2
+  end.
+
+Definition is_value (t : term) :=
+  if_value t True False.
+
+Hint Extern 1 (is_value _) => (simpl; tauto) : is_value obvious.
+
+(* A term either is or is not a value. *)
+
+Lemma value_or_nonvalue:
+  forall t,
+  is_value t \/ ~ is_value t.
+Proof.
+  destruct t; simpl; eauto.
+Qed.
+
+(* Simplification rules for [if_value]. *)
+
+Lemma if_value_value:
+  forall A v (a1 a2 : A),
+  is_value v ->
+  if_value v a1 a2 = a1.
+Proof.
+  destruct v; simpl; tauto.
+Qed.
+
+Lemma if_value_nonvalue:
+  forall A t (a1 a2 : A),
+  ~ is_value t ->
+  if_value t a1 a2 = a2.
+Proof.
+  destruct t; simpl; tauto.
+Qed.
+
+(* The syntactic subcategory of values is preserved by renamings. *)
+
+Lemma is_value_renaming:
+  forall v xi,
+  is_value v ->
+  is_value v.[ren xi].
+Proof.
+  destruct v; simpl; eauto.
+Qed.
+
+Lemma is_nonvalue_renaming:
+  forall v xi,
+  ~ is_value v ->
+  ~ is_value v.[ren xi].
+Proof.
+  destruct v; simpl; eauto.
+Qed.
+
+Hint Resolve is_value_renaming is_nonvalue_renaming : is_value obvious.
+
+Ltac is_value :=
+  eauto with is_value.
+
+(* The tactic [not_a_value] can be used to prove that the current case
+   is impossible, because we have a hypothesis of the form [~ is_value v],
+   where [v] clearly is a value. *)
+
+Ltac not_a_value :=
+  solve [ false; is_value ].
+
+Ltac if_value :=
+  repeat first [ rewrite if_value_value by is_value |
+                 rewrite if_value_nonvalue by is_value ].
+
+(* The tactic [value_or_nonvalue t] creates two cases: either [t] is a value,
+   or it isn't. *)
+
+Ltac value_or_nonvalue t :=
+  destruct (value_or_nonvalue t);
+  if_value.
+
+(* The tactic [value_or_app_or_let] creates three cases: either [t] is a value,
+   or it is an application, or it is a [let] construct. *)
+
+Ltac value_or_app_or_let t :=
+  value_or_nonvalue t; [|
+    destruct t as [ ? | ? | t1 t2 | t1 t2 ]; [ not_a_value | not_a_value | |]
+      (* In principle, we should not fix the names [t1] and [t2] here,
+         as it might cause name clashes. *)
+  ].
+
+(* The predicate [is_value_subst sigma] holds if every term in the
+   codomain of the substitution [sigma] is a value. *)
+
+Definition is_value_subst (sigma : var -> term) :=
+  forall x, is_value (sigma x).
+
+Lemma is_value_subst_ids:
+  is_value_subst ids.
+Proof.
+  intros x. is_value.
+Qed.
+
+Lemma is_value_subst_cons:
+  forall v sigma,
+  is_value v ->
+  is_value_subst sigma ->
+  is_value_subst (v .: sigma).
+Proof.
+  intros. intros [|x]; is_value.
+Qed.
+
+Definition is_value_subst_up:
+  forall sigma,
+  is_value_subst sigma ->
+  is_value_subst (up sigma).
+Proof.
+  intros sigma h. intros [|x]; asimpl.
+  { simpl. eauto. }
+  { is_value. }
+Qed.
+
+Definition is_value_subst_upn:
+  forall sigma i,
+  is_value_subst sigma ->
+  is_value_subst (upn i sigma).
+Proof.
+  induction i; intros; asimpl.
+  { eauto. }
+  { rewrite <- fold_up_upn. eauto using is_value_subst_up. }
+Qed.
+
+Lemma is_value_subst_renaming:
+  forall sigma i,
+  is_value_subst sigma ->
+  is_value_subst (sigma >> ren (+i)).
+Proof.
+  intros. intro x. asimpl. is_value.
+Qed.
+
+Hint Resolve is_value_subst_up is_value_subst_upn is_value_subst_renaming
+  : is_value obvious.
+
+Lemma values_are_preserved_by_value_substitutions:
+  forall v sigma,
+  is_value v ->
+  is_value_subst sigma ->
+  is_value v.[sigma].
+Proof.
+  destruct v; simpl; intros; eauto with is_value.
+Qed.
+
+Lemma nonvalues_are_preserved_by_substitutions:
+  forall t sigma,
+  ~ is_value t ->
+  ~ is_value t.[sigma].
+Proof.
+  destruct t; simpl; tauto.
+Qed.
+
+Hint Resolve
+  is_value_subst_ids
+  is_value_subst_cons
+  values_are_preserved_by_value_substitutions
+  nonvalues_are_preserved_by_substitutions
+: is_value obvious.
+
+Lemma is_ren_is_value_subst:
+  forall sigma,
+  is_ren sigma ->
+  is_value_subst sigma.
+Proof.
+  intros ? [ xi ? ]. subst. eauto with is_value.
+Qed.
+
+Hint Resolve is_ren_is_value_subst : is_value obvious.
diff --git a/coq/Option.v b/coq/Option.v
new file mode 100644
index 0000000..5ed2a2e
--- /dev/null
+++ b/coq/Option.v
@@ -0,0 +1,120 @@
+(* -------------------------------------------------------------------------- *)
+
+(* The [bind] combinator of the option monad. *)
+
+Definition bind {A B} (f : option A) (k : A -> option B) : option B :=
+  match f with
+  | None =>
+      None
+  | Some a =>
+      k a
+  end.
+
+(* The standard syntactic sugar for [bind]. [f >>= k] can be read as ``first
+   do [f]; then, if successful, with the result of [f], do [k]''. *)
+
+Notation "f >>= k" := (bind f k) (at level 55).
+
+(* -------------------------------------------------------------------------- *)
+
+(* These lemmas help prove an equation of the form [f >>= k = b]. *)
+
+Lemma prove_bind_None:
+  forall {A B} {f} {k : A -> option B},
+  f = None ->
+  f >>= k = None.
+Proof.
+  intros. subst. eauto.
+Qed.
+
+Lemma prove_bind_Some:
+  forall {A B} {f} {k : A -> option B} {a b},
+  f = Some a ->
+  k a = b ->
+  f >>= k = b.
+Proof.
+  intros. subst. eauto.
+Qed.
+
+(* This lemma helps exploit an equation of the form [f >>= k = Some b]. *)
+
+Lemma invert_bind_Some:
+  forall {A B} {f} {k : A -> option B} {b},
+  f >>= k = Some b ->
+  exists a, f = Some a /\ k a = Some b.
+Proof.
+  destruct f; simpl; intros.
+  { eauto. }
+  { congruence. }
+Qed.
+
+Ltac invert_bind_Some :=
+  match goal with
+  h: ?f >>= _ = Some _ |- _ =>
+    let heq := fresh in
+    generalize (invert_bind_Some h); clear h; intros (?&?&h)
+  end.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The standard ordering on options, where [None] is less defined then
+   everything, and every element of the form [Some a] is less defined
+   than itself only. *)
+
+Definition less_defined {A} (o1 o2 : option A) :=
+  forall a, o1 = Some a -> o2 = Some a.
+
+(* -------------------------------------------------------------------------- *)
+
+(* This lemma exploits an assertion of the form [less_defined (Some _) _]. *)
+
+Lemma invert_less_defined_Some:
+  forall {A} {a : A} {o : option A},
+  less_defined (Some a) o ->
+  Some a = o.
+Proof.
+  unfold less_defined. intros. symmetry. eauto.
+Qed.
+
+Ltac invert_less_defined :=
+  match goal with
+  | h: less_defined (Some _) _ |- _ =>
+      generalize (invert_less_defined_Some h); clear h; intro h
+  end.
+
+(* -------------------------------------------------------------------------- *)
+
+(* These lemmas help prove assertions of the form [less_defined _ _]. *)
+
+Lemma prove_less_defined_None:
+  forall {A} {o : option A},
+  less_defined None o.
+Proof.
+  unfold less_defined. intros. congruence.
+Qed.
+
+Lemma reflexive_less_defined:
+  forall {A} {o : option A},
+  less_defined o o.
+Proof.
+  unfold less_defined. eauto.
+Qed.
+
+Local Hint Extern 1 (_ <> _) => congruence : congruence.
+
+Lemma prove_less_defined_bind:
+  forall {A B} {f1 f2 : option A} {k1 k2 : A -> option B},
+  less_defined f1 f2 ->
+  (f1 <> None -> forall a, less_defined (k1 a) (k2 a)) ->
+  less_defined (f1 >>= k1) (f2 >>= k2).
+Proof.
+  intros. destruct f1; simpl in *.
+  (* Case: [f1] is [Some _]. *)
+  { invert_less_defined. subst. simpl. eauto with congruence. }
+  (* Case: [f1] is [None]. *)
+  { eauto using prove_less_defined_None. }
+Qed.
+
+Hint Resolve
+  prove_less_defined_None reflexive_less_defined prove_less_defined_bind
+: less_defined.
diff --git a/coq/Sequences.v b/coq/Sequences.v
new file mode 100644
index 0000000..fb5a3ca
--- /dev/null
+++ b/coq/Sequences.v
@@ -0,0 +1,321 @@
+(** A library of relation operators defining sequences of transitions
+    and useful properties about them. Originally by Xavier Leroy, with
+    some improvements and additions by François Pottier. *)
+
+Set Implicit Arguments.
+
+Section SEQUENCES.
+
+Variable A: Type.
+
+Implicit Types R S : A -> A -> Prop.
+Implicit Types P   : A -> Prop.
+
+(** Zero, one or several transitions: reflexive, transitive closure of [R]. *)
+
+Inductive star R : A -> A -> Prop :=
+| star_refl:
+    forall a,
+    star R a a
+| star_step:
+    forall a b c,
+    R a b -> star R b c -> star R a c.
+
+Hint Constructors star.
+
+Lemma star_refl_eq:
+  forall R a b, a = b -> star R a b.
+Proof.
+  intros. subst. eauto.
+Qed.
+
+Lemma star_one:
+  forall R a b, R a b -> star R a b.
+Proof.
+  eauto.
+Qed.
+
+Lemma star_trans:
+  forall R a b, star R a b ->
+  forall c, star R b c -> star R a c.
+Proof.
+  induction 1; eauto.
+Qed.
+
+Lemma star_covariant:
+  forall R S,
+  (forall a b, R a b -> S a b) ->
+  (forall a b, star R a b -> star S a b).
+Proof.
+  induction 2; eauto.
+Qed.
+
+(* If [R] preserves some property [P], then [star R] preserves [P]. *)
+
+Lemma star_implication:
+  forall P R,
+  (forall a1 a2, R a1 a2 -> P a1 -> P a2) ->
+  (forall a1 a2, star R a1 a2 -> P a1 -> P a2).
+Proof.
+  induction 2; eauto.
+Qed.
+
+(* The same implication holds in the reverse direction (right to left). *)
+
+Lemma star_implication_reversed:
+  forall P R,
+  (forall a1 a2, R a1 a2 -> P a2 -> P a1) ->
+  (forall a1 a2, star R a1 a2 -> P a2 -> P a1).
+Proof.
+  induction 2; eauto.
+Qed.
+
+(** One or several transitions: transitive closure of [R]. *)
+
+Inductive plus R: A -> A -> Prop :=
+| plus_left:
+    forall a b c,
+    R a b -> star R b c -> plus R a c.
+
+Hint Constructors plus.
+
+Lemma plus_one:
+  forall R a b, R a b -> plus R a b.
+Proof.
+  eauto.
+Qed.
+
+Lemma plus_star:
+  forall R a b, plus R a b -> star R a b.
+Proof.
+  inversion 1; eauto.
+Qed.
+
+Lemma plus_covariant:
+  forall R S,
+  (forall a b, R a b -> S a b) ->
+  (forall a b, plus R a b -> plus S a b).
+Proof.
+  induction 2; eauto using star_covariant.
+Qed.
+
+(* A direct induction principle for [plus]: when [plus R a b] holds,
+   either there is just one step, or there is one, followed with more. *)
+
+Lemma plus_ind_direct:
+  forall R P : A -> A -> Prop,
+  (forall a b, R a b -> P a b) ->
+  (forall a b c, R a b -> plus R b c -> P b c -> P a c) ->
+  forall a b, plus R a b -> P a b.
+Proof.
+  intros ? ? Hone Hmore a c Hplus. destruct Hplus as [ ? b ? hR hRStar ].
+  generalize b c hRStar a hR.
+  clear b c hRStar a hR.
+  induction 1; eauto.
+Qed.
+
+Lemma plus_star_trans:
+  forall R a b c, plus R a b -> star R b c -> plus R a c.
+Proof.
+  inversion 1; eauto using star_trans.
+Qed.
+
+Lemma star_plus_trans:
+  forall R a b c, star R a b -> plus R b c -> plus R a c.
+Proof.
+  inversion 1; inversion 1; eauto using star_trans.
+Qed.
+
+Lemma plus_trans:
+  forall R a b c, plus R a b -> plus R b c -> plus R a c.
+Proof.
+  eauto using plus_star_trans, plus_star.
+Qed.
+
+Lemma plus_right:
+  forall R a b c, star R a b -> R b c -> plus R a c.
+Proof.
+  eauto using star_plus_trans.
+Qed.
+
+(** Absence of transitions. *)
+
+Definition irred R a :=
+  forall b, ~ R a b.
+
+Definition halts R a :=
+  exists b, star R a b /\ irred R b.
+
+(** Infinitely many transitions. *)
+
+CoInductive infseq R : A -> Prop :=
+| infseq_step:
+    forall a b,
+    R a b -> infseq R b -> infseq R a.
+
+(** Properties of [irred]. *)
+
+Lemma irred_irred:
+  forall R t1 u1,
+  irred R t1 ->
+  (forall u2, R u1 u2 -> exists t2, R t1 t2) ->
+  irred R u1.
+Proof.
+  unfold irred. intros ? ? ? Hirred Himpl u2 Hu2.
+  destruct (Himpl _ Hu2) as [ t2 Ht2 ].
+  eapply Hirred. eauto.
+Qed.
+
+Lemma irreducible_terms_do_not_reduce:
+  forall R a b, irred R a -> R a b -> False.
+Proof.
+  unfold irred, not. eauto.
+Qed.
+
+(** Coinduction principles to show the existence of infinite sequences. *)
+
+Lemma infseq_coinduction_principle:
+  forall R P,
+  (forall a, P a -> exists b, R a b /\ P b) ->
+  forall a, P a -> infseq R a.
+Proof.
+  intros ? ? Hstep. cofix COINDHYP; intros a hPa.
+  destruct (Hstep a hPa) as (?&?&?).
+  econstructor; eauto.
+Qed.
+
+Lemma infseq_coinduction_principle_2:
+  forall R P a,
+  P a ->
+  (forall a, P a -> exists b, plus R a b /\ P b) ->
+  infseq R a.
+Proof.
+  intros ? ? ? ? Hinv.
+  apply infseq_coinduction_principle with
+    (P := fun a => exists b, star R a b /\ P b).
+  (* Proof that the invariant is preserved. *)
+  { clear dependent a.
+    intros a (b&hStar&hPb).
+    inversion hStar; subst.
+    { destruct (Hinv b hPb) as [c [hPlus ?]].
+      inversion hPlus; subst. eauto. }
+    { eauto. }
+  }
+  (* Proof that the invariant initially holds. *)
+  { eauto. }
+Qed.
+
+Lemma infseq_plus:
+  forall R a,
+  infseq (plus R) a ->
+  infseq R a.
+Proof.
+  intros. eapply infseq_coinduction_principle_2
+    with (P := fun a => infseq (plus R) a).
+  { eauto. }
+  clear dependent a. intros a hInfSeq.
+  destruct hInfSeq. eauto.
+Qed.
+
+(** An example of use of [infseq_coinduction_principle]. *)
+
+Lemma infseq_alternate_characterization:
+  forall R a,
+  (forall b, star R a b -> exists c, R b c) ->
+  infseq R a.
+Proof.
+  intros R. apply infseq_coinduction_principle.
+  intros a Hinv. destruct (Hinv a); eauto.
+Qed.
+
+Lemma infseq_covariant:
+  forall R S,
+  (forall a b, R a b -> S a b) ->
+  forall a, infseq R a -> infseq S a.
+Proof.
+  intros. eapply infseq_coinduction_principle
+  with (P := fun a => infseq R a); [| eauto ].
+  clear dependent a. intros a hInfSeq.
+  destruct hInfSeq. eauto.
+Qed.
+
+(** A sequence either is infinite or stops on an irreducible term.
+    This property needs excluded middle from classical logic. *)
+
+Require Import Classical.
+
+Lemma infseq_or_finseq:
+  forall R a,
+  infseq R a \/ halts R a.
+Proof.
+  intros.
+  destruct (classic (forall b, star R a b -> exists c, R b c)).
+  { left. eauto using infseq_alternate_characterization. }
+  { right.
+    destruct (not_all_ex_not _ _ H) as [b Hb].
+    destruct (imply_to_and _ _ Hb).
+    unfold halts, irred, not. eauto. }
+Qed.
+
+(** Additional properties for deterministic transition relations. *)
+
+Section DETERMINISM.
+
+Variable R : A -> A -> Prop.
+
+Hypothesis R_determ: forall a b c, R a b -> R a c -> b = c.
+
+Ltac R_determ :=
+  match goal with h1: R ?a ?b1, h2: R ?a ?b2 |- _ =>
+    assert (b1 = b2); [ eauto | subst ]
+  end.
+
+(** Uniqueness of transition sequences. *)
+
+Lemma star_star_inv:
+  forall a b, star R a b -> forall c, star R a c -> star R b c \/ star R c b.
+Proof.
+  induction 1; inversion 1; intros; subst; try R_determ; eauto.
+Qed.
+
+Lemma finseq_unique:
+  forall a b b',
+  star R a b -> irred R b ->
+  star R a b' -> irred R b' ->
+  b = b'.
+Proof.
+  unfold irred, not.
+  intros ? ? ? Hab Hirred Hab' Hirred'.
+  destruct (star_star_inv Hab Hab') as [ Hbb' | Hbb' ];
+  inversion Hbb'; subst;
+  solve [ eauto | elimtype False; eauto ].
+Qed.
+
+Lemma infseq_star_inv:
+  forall a b, star R a b -> infseq R a -> infseq R b.
+Proof.
+  induction 1; inversion 1; intros; try R_determ; eauto.
+Qed.
+
+Lemma infseq_finseq_excl:
+  forall a b,
+  star R a b -> irred R b -> infseq R a -> False.
+Proof.
+  unfold irred, not. intros.
+  assert (h: infseq R b). { eauto using infseq_star_inv. }
+  inversion h. eauto.
+Qed.
+
+Lemma infseq_halts_excl:
+  forall a,
+  halts R a -> infseq R a -> False.
+Proof.
+  intros ? (?&?&?). eauto using infseq_finseq_excl.
+Qed.
+
+End DETERMINISM.
+
+End SEQUENCES.
+
+Hint Resolve star_refl star_step star_one star_trans plus_left plus_one
+             plus_star plus_star_trans star_plus_trans plus_right: sequences.