diff --git a/src/chap11.v b/src/chap11.v
index 4982e4e..9bccfe6 100644
--- a/src/chap11.v
+++ b/src/chap11.v
@@ -6,11 +6,12 @@ From Stdlib Require Import
   FSets.FMapList
   FSets.FMapFacts
   Structures.OrderedTypeEx
+  Structures.OrderedType
   Nat
   Arith
+  Compare_dec
   Lia.
 Import ListNotations.
-Require Import Recdef.
 
 Open Scope string_scope.
 
@@ -21,14 +22,88 @@ Module Chap11.
           and adapted to fit the contents from the book.
   *)
 
-  Definition varname := string.
+  Inductive varname : Type :=
+    | varname_nat : nat -> varname
+    | varname_unused : varname.
+
+  Scheme Equality for varname.
+
+  Module Varname_as_OT <: OrderedType.
+    Definition t := varname.
+
+    Definition eq := @eq t.
+
+    Definition lt (x y : t) := match x, y with
+      | varname_nat n1, varname_nat n2 => n1 < n2
+      | varname_unused, varname_nat _ => True
+      | varname_nat _, varname_unused => False
+      | varname_unused, varname_unused => False
+      end.
+
+    Definition eq_refl := @eq_refl t.
+    Definition eq_sym := @eq_sym t.
+    Definition eq_trans := @eq_trans t.
+
+    Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+    Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+    Parameter compare : forall x y : t, Compare lt eq x y.
+    Parameter eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
+  End Varname_as_OT.
+
+  (* Module Varname_as_OT_Facts := OrderedTypeFacts Varname_as_OT. *)
+
+  Definition varname_eqb (x y : varname) : bool :=
+    match x, y with
+    | varname_nat n1, varname_nat n2 => Nat.eqb n1 n2
+    | varname_unused, varname_unused => true
+    | _, _ => false
+    end.
+
+  Lemma varname_eqb_spec s1 s2 : Bool.reflect (s1 = s2) (varname_eqb s1 s2).
+  Proof.
+    destruct s1, s2; simpl.
+  Admitted.
+
+  Lemma varname_eqb_neq : forall (x y : varname),
+    varname_eqb x y = false <-> ~ Varname_as_OT.eq x y.
+  Proof.
+    intros x y. split; intros H.
+    - destruct x, y; simpl in *; try discriminate; try congruence.
+      apply Nat.eqb_neq in H. congruence.
+    - destruct x, y; simpl in *; try reflexivity; try congruence.
+      apply Nat.eqb_neq. congruence.
+  Qed.
+
+  Fixpoint repeat_string (s : string) (n : nat) : string :=
+    match n with
+    | 0 => ""
+    | S n' => s ++ repeat_string s n'
+    end.
+
+  Definition varname_to_string (v : varname) : string :=
+    match v with
+    | varname_nat n => "x" ++ repeat_string "'" n
+    | varname_unused => "_"
+    end.
+
+  Fixpoint max_varname (s : set varname) : nat :=
+    match s with
+    | [] => 0
+    | varname_nat n :: s' => Nat.max n (max_varname s')
+    | varname_unused :: s' => max_varname s'
+    end.
+
+  Definition fresh_varname (s : set varname) : varname :=
+    varname_nat (S (max_varname s)).
+
+  Definition typename := string.
   Definition record_label := string.
 
   Inductive type : Type :=
     (** T1 -> T2 *)
     | type_Arrow : type -> type -> type
     (** ArbitraryType *)
-    | type_Base : string -> type
+    | type_Base : typename -> type
     (** T1 x T2 *)
     | type_Product : type -> type -> type
     (** {T1, T2, ..., Tn} *)
@@ -38,13 +113,15 @@ Module Chap11.
     (** T1 + T2 *)
     | type_Sum : type -> type -> type
     (** <l1 : T1, l2 : T2, ..., ln : Tn> *)
-    | type_Variant : list (record_label * type) -> type.
+    | type_Variant : list (record_label * type) -> type
+    (** List[T] *)
+    | type_List : type -> type.
 
   Definition type_Bool := type_Base "Bool".
   Definition type_Unit := type_Base "Unit".
 
-  Module M := FMapList.Make(String_as_OT).
-  Module MFacts := FMapFacts.WFacts_fun String_as_OT M.
+  Module M := FMapList.Make(Varname_as_OT).
+  Module MFacts := FMapFacts.WFacts_fun Varname_as_OT M.
   Definition context := M.t type.
   Definition empty_ctx : context := @M.empty type.
 
@@ -101,19 +178,30 @@ Module Chap11.
     | term_variant_case : term -> list (record_label * varname * term) -> term
 
     (** fix t *)
-    | term_fix : term -> term.
+    | term_fix : term -> term
+
+    (** nil[T] *)
+    | term_nil : type -> term
+    (** cons[T] t1 t2 *)
+    | term_cons : type -> term -> term -> term
+    (** is_nil[T] t *)
+    | term_is_nil : type -> term -> term
+    (** head[T] t *)
+    | term_head : type -> term -> term
+    (** tail[T] t *)
+    | term_tail : type -> term -> term.
 
   (* Although we don't have syntax sugar because we omit "Notation",
       we can simply define a function that looks like a "term_" constructor
       to simulate it *)
   Definition term_seq (t1 t2 : term) : term :=
-    term_app (term_abs "_" type_Unit t2) t1.
+    term_app (term_abs varname_unused type_Unit t2) t1.
 
-  Definition term_letrec (x : string) (T1 : type) (t1 : term) (t2 : term) : term :=
+  Definition term_letrec (x : varname) (T1 : type) (t1 : term) (t2 : term) : term :=
     term_let x (term_fix (term_abs x T1 t1)) t2.
 
   Inductive is_value : term -> Prop :=
-    | v_abs : forall (x : string) (T2 : type) (t1 : term),
+    | v_abs : forall (x : varname) (T2 : type) (t1 : term),
         is_value (term_abs x T2 t1)
     | v_true :
         is_value term_true
@@ -139,20 +227,25 @@ Module Chap11.
         is_value (term_inr v T)
     | v_variant : forall (l : record_label) (v : term) (T : type),
         is_value v ->
-        is_value (term_variant l v T).
+        is_value (term_variant l v T)
+    | v_nil : forall (T : type),
+        is_value (term_nil T)
+    | v_cons : forall (T : type) (v1 v2 : term),
+        is_value v1 ->
+        is_value v2 ->
+        is_value (term_cons T v1 v2).
 
   Inductive is_pattern : term -> Prop :=
-    | p_var : forall (x : string),
+    | p_var : forall (x : varname),
         is_pattern (term_var x)
     | p_pattern_bind : forall (t1 t2 t3 : term),
         is_pattern t1 ->
         is_pattern (term_pattern_bind t1 t2 t3).
 
-  (* Before we continue with evaluation and typing rules,
-     we need substitution. After chapter 6, it seems like tapl
-     assumes that our substitution function is capture-avoiding,
-     so this is a requirement *)
-  Inductive is_free_variable : string -> term -> Prop :=
+  (* This denotes whether a variable is free in a term.
+     That is, there is no closure in t that will eventually
+     replace the variable *)
+  Inductive is_free_variable : varname -> term -> Prop :=
     | FV_Var : forall x,
         is_free_variable x (term_var x)
 
@@ -220,78 +313,51 @@ Module Chap11.
         is_free_variable x (term_record_proj t k).
     (* TODO: expand me, and double check that the above is correct *)
 
-
-  (* In order to generate fresh names, we need to define a function that
-     generates names based on the ones it can already see in the term.
-     This is problematic to do in a normal fixpoint, because we need the
-     function to have a measure that is strictly decreasing.
-     
-     In this implementation, we append primes to x until we find an emtpy
-     one. Our strictly decreasing measure is the max count of primes of any
-     'x' in the set of free variables.
-  *)
-
-  Fixpoint repeat_n (x : string) (n : nat) : string :=
-    match n with
-    | 0 => x
-    | S n' => x ++ repeat_n x n'
+  Fixpoint varnames (t : term) : (set varname) :=
+    match t with
+      | term_var y => [y]
+      | term_abs y T t1 => set_union varname_eq_dec [y] (varnames t1)
+      | term_app t1 t2 => set_union varname_eq_dec (varnames t1) (varnames t2)
+      | term_true => []
+      | term_false => []
+      | term_unit => []
+      | term_if t1 t2 t3 => set_union varname_eq_dec (varnames t1) (set_union varname_eq_dec (varnames t2) (varnames t3))
+      | term_ascribe t1 T => varnames t1
+      | term_let y t1 t2 => set_union varname_eq_dec [y] (set_union varname_eq_dec (varnames t1) (varnames t2))
+      | term_pair t1 t2 => set_union varname_eq_dec (varnames t1) (varnames t2)
+      | term_fst t1 => varnames t1
+      | term_snd t1 => varnames t1
+      | term_tuple ts => fold_left (fun acc t => set_union varname_eq_dec acc (varnames t)) ts []
+      | term_tuple_proj t n => varnames t
+      | term_record m => fold_left (fun acc kv => set_union varname_eq_dec acc (varnames (snd kv))) m []
+      | term_record_proj t k => varnames t
+      | term_pattern_bind p t1 t2 => set_union varname_eq_dec (varnames p) (set_union varname_eq_dec (varnames t1) (varnames t2))
+      | term_inl t1 T => varnames t1
+      | term_inr t1 T => varnames t1
+      | term_case t0 T x t1 y t2 => set_union varname_eq_dec (varnames t0) (set_union varname_eq_dec [x] (set_union varname_eq_dec (varnames t1) (set_union varname_eq_dec [y] (varnames t2))))
+      | term_variant l t1 T => varnames t1
+      | term_variant_case t0 cases => set_union varname_eq_dec (varnames t0) (fold_left (fun acc case => let '(l, x, t) := case in set_union varname_eq_dec acc (set_union varname_eq_dec [x] (varnames t))) cases [])
+      | term_fix t1 => varnames t1
+      | term_nil T => []
+      | term_cons T t1 t2 => set_union varname_eq_dec (varnames t1) (varnames t2)
+      | term_is_nil T t1 => varnames t1
+      | term_head T t1 => varnames t1
+      | term_tail T t1 => varnames t1
     end.
 
-  Fixpoint max_key_len (xs : list (string * type)) : nat :=
-    match xs with
-    | [] => 0
-    | (k, _) :: xs' =>
-        Nat.max (String.length k) (max_key_len xs')
-    end.
+  Lemma fresh_varname_not_free : forall (t : term) (x : varname),
+    fresh_varname (varnames t) = x <-> ~ is_free_variable x t.
+  Proof. Admitted.
 
-  Definition decrement_key (k : string) : option string :=
-    match String.length k with
-    | 0 => None
-    | 1 => None
-    | S n => Some (String.substring 0 n k)
-    end.
-
-  (* Function fresh_var
-    (Γ : context)
-    {measure max_key_len (M.elements Γ)}
-    : string :=
-    if M.mem "x" Γ then
-      let
-        reduced_keys : context := M.remove "x" (filtermap (fun '(k, _) => decrement_key k) (M.elements Γ))
-      in
-      fresh_var reduced_keys
-    else
-      "x".
-  Proof. *)
-
-  (* Function fresh_varname
-    (x : string)
-    (s : set string)
-    {measure max_varname_size s}
-    : string :=
-    match s with
-    | [] => x
-    | y :: ys =>
-        if String.eqb x y
-          then fresh_varname (x ++ "'") (decrease_varname_sizes ys)
-          else fresh_varname x ys
-    end.
-  Proof.
-    intros x s y ys.
-    - unfold decrease_varname_sizes.
-    lia. *)
-
-
-
-  Fixpoint substitute (x : string) (s : term) (t : term) : term :=
+  Fixpoint substitute (x : varname) (s : term) (t : term) : term :=
     let f := fun t => substitute x s t in
     match t with
-    | term_var y =>
-        if String.eqb x y
+      | term_var y =>
+        if varname_eqb x y
           then s
           else t
-    | term_abs y T t1 =>
-        if String.eqb x y
+      | term_abs y T t1 =>
+        if varname_eqb x y
           then t
           else term_abs y T (f t1)
     | term_app t1 t2 => term_app (f t1) (f t2)
@@ -301,7 +367,7 @@ Module Chap11.
     | term_if t1 t2 t3 => term_if (f t1) (f t2) (f t3)
     | term_ascribe t1 T => term_ascribe (f t1) T
     | term_let y t1 t2 =>
-        if String.eqb x y
+        if varname_eqb x y
           then term_let y (f t1) t2
           else term_let y (f t1) (f t2)
     | term_pair t1 t2 => term_pair (f t1) (f t2)
@@ -319,11 +385,16 @@ Module Chap11.
     | term_variant_case t0 cases =>
         term_variant_case (f t0) (map (fun '(l, x, t) => (l, x, f t)) cases)
     | term_fix t1 => term_fix (f t1)
+    | term_nil T => term_nil T
+    | term_cons T t1 t2 => term_cons T (f t1) (f t2)
+    | term_is_nil T t1 => term_is_nil T (f t1)
+    | term_head T t1 => term_head T (f t1)
+    | term_tail T t1 => term_tail T (f t1)
     end.
 
   Inductive matching : term -> term -> term -> Prop :=
     (** match(x, 5) -> [x -> 5] *)
-    | M_Var : forall (x : string) (v : term),
+    | M_Var : forall (x : varname) (v : term),
         is_pattern (term_var x) ->
         matching (term_var x) v (substitute x v (term_var x)).
     (** match({x, y}, {5, true}) -> [x -> 5, y -> true]
@@ -339,12 +410,12 @@ Module Chap11.
           step t2 t2' ->
           step (term_app v1 t2) (term_app v1 t2')
 
-    | E_AppAbs : forall (x : string) (T : type) (t v : term),
+    | E_AppAbs : forall (x : varname) (T : type) (t v : term),
           is_value v ->
           step (term_app (term_abs x T t) v) (substitute x v t)
 
     | E_Wildcard : forall (t1 t2 : term),
-          step (term_app (term_abs "_" type_Unit t1) t2) t1
+          step (term_app (term_abs varname_unused type_Unit t1) t2) t1
 
     | E_IfTrue : forall (t1 t2 : term),
         step (term_if term_true t1 t2) t1
@@ -361,10 +432,10 @@ Module Chap11.
         step t t' ->
         step (term_ascribe t T) (term_ascribe t' T)
 
-    | E_LetV : forall (x : string) (v t2 : term),
+    | E_LetV : forall (x : varname) (v t2 : term),
         is_value v ->
         step (term_let x v t2) (substitute x v t2)
-    | E_Let : forall (x : string) (t1 t1' t2 : term),
+    | E_Let : forall (x : varname) (t1 t1' t2 : term),
         step t1 t1' ->
         step (term_let x t1 t2) (term_let x t1' t2)
 
@@ -400,17 +471,14 @@ Module Chap11.
         step (term_tuple_proj t1 n) (term_tuple_proj t1' n)
     | E_Tuple : forall (t : list term) (tj tj' : term) (j : nat),
         (* j is bounded by the length of the tuple *)
-        0 <= j < length t ->
+        j < length t ->
         (* All terms before j are values *)
-        (forall i,
-          1 <= i < j ->
-          i < length t ->
-          is_value (nth i t term_unit)) ->
+        Forall is_value (firstn j t) ->
         (* j-th element is an evaluatable term *)
         tj = nth j t term_unit ->
         step tj tj' ->
         (* t' is the tuple with the j-th element replaced by tj' *)
-        let t' := List.app (firstn j t) (nth j t term_unit :: (skipn (S j) t)) in
+        let t' := List.app (firstn j t) (tj' :: (skipn (S j) t)) in
         step (term_tuple t) (term_tuple t')
 
     | E_ProjRcd : forall (k : record_label) (v : term) (m : list (record_label * term)),
@@ -420,14 +488,11 @@ Module Chap11.
     | E_Proj' : forall (t1 t1' : term) (k : record_label),
         step t1 t1' ->
         step (term_record_proj t1 k) (term_record_proj t1' k)
-    | E_Rcd : forall (r : list (string * term)) (tj tj' : term) (j : nat),
+    | E_Rcd : forall (r : list (record_label * term)) (tj tj' : term) (j : nat),
         (* j is bounded by the length of the record *)
-        1 <= j <= length r ->
+        j < length r ->
         (* All terms before j are values *)
-        (forall i,
-          1 <= i < j ->
-          i < length r ->
-          is_value (snd (nth i r ("", term_unit)))) ->
+        Forall is_value (firstn j (map snd r)) ->
         (* j-th element is an evaluatable term *)
         tj = snd (nth j r ("", term_unit)) ->
         step tj tj' ->
@@ -447,13 +512,13 @@ Module Chap11.
         step t1 t1' ->
         step (term_pattern_bind p t1 t2) (term_pattern_bind p t1' t2)
 
-    | E_CaseInl : forall (v t1 t2 : term) (T : type) (x y : string),
+    | E_CaseInl : forall (v t1 t2 : term) (T : type) (x y : varname),
         is_value v ->
         step (term_case (term_inl v T) T x t1 y t2) (substitute x v t1)
-    | E_CaseInr : forall (v t1 t2 : term) (T : type) (x y : string),
+    | E_CaseInr : forall (v t1 t2 : term) (T : type) (x y : varname),
         is_value v ->
         step (term_case (term_inr v T) T x t1 y t2) (substitute y v t2)
-    | E_Case : forall (t t' t1 t2 : term) (T : type) (x y : string),
+    | E_Case : forall (t t' t1 t2 : term) (T : type) (x y : varname),
         step t t' ->
         step (term_case t T x t1 y t2) (term_case t' T x t1 y t2)
     | E_Inl : forall (t t' : term) (T : type),
@@ -463,7 +528,7 @@ Module Chap11.
         step t t' ->
         step (term_inr t T) (term_inr t' T)
 
-    | E_CaseVariant : forall (Γ : context) (lj xj : record_label) (vj tj : term) (T : type) (c : list (record_label * varname * term)),
+    | E_CaseVariant : forall (Γ : context) (lj : record_label) (xj : varname) (vj tj : term) (T : type) (c : list (record_label * varname * term)),
         is_value vj ->
         In (lj, xj, tj) c ->
         step (term_variant_case (term_variant lj vj T) c) (substitute xj vj tj)
@@ -474,18 +539,49 @@ Module Chap11.
         step t t' ->
         step (term_variant l t T) (term_variant l t' T)
 
-    | E_FixBeta : forall (x : string) (T1 : type) (t2 : term),
+    | E_FixBeta : forall (x : varname) (T1 : type) (t2 : term),
         step (term_fix (term_abs x T1 t2)) (substitute x (term_fix (term_abs x T1 t2)) t2)
     | E_Fix : forall (t t' : term),
         step t t' ->
-        step (term_fix t) (term_fix t').
+        step (term_fix t) (term_fix t')
+
+    | E_Cons1 : forall (T : type) (t1 t1' t2 : term),
+        step t1 t1' ->
+        step (term_cons T t1 t2) (term_cons T t1' t2)
+    | E_Cons2 : forall (T : type) (v1 t2 t2' : term),
+        is_value v1 ->
+        step t2 t2' ->
+        step (term_cons T v1 t2) (term_cons T v1 t2')
+    | E_IsNilNil : forall (T : type),
+        step (term_is_nil T (term_nil T)) term_true
+    | E_IsNilCons : forall (T : type) (v1 v2 : term),
+        is_value v1 ->
+        is_value v2 ->
+        step (term_is_nil T (term_cons T v1 v2)) term_false
+    | E_IsNil : forall (T : type) (t t' : term),
+        step t t' ->
+        step (term_is_nil T t) (term_is_nil T t')
+    | E_HeadCons : forall (T : type) (v1 v2 : term),
+        is_value v1 ->
+        is_value v2 ->
+        step (term_head T (term_cons T v1 v2)) v1
+    | E_Head : forall (T : type) (t t' : term),
+        step t t' ->
+        step (term_head T t) (term_head T t')
+    | E_TailCons : forall (T : type) (v1 v2 : term),
+        is_value v1 ->
+        is_value v2 ->
+        step (term_tail T (term_cons T v1 v2)) v2
+    | E_Tail : forall (T : type) (t t' : term),
+        step t t' ->
+        step (term_tail T t) (term_tail T t').
 
   Inductive has_type : context -> term -> type -> Prop :=
-    | T_Var : forall (Γ : context) (x : string) (T1 : type),
+    | T_Var : forall (Γ : context) (x : varname) (T1 : type),
         M.find x Γ = Some T1 ->
         has_type Γ (term_var x) T1
 
-    | T_Abs : forall (Γ : context) (x : string) (T1 T2 : type) (t1 : term),
+    | T_Abs : forall (Γ : context) (x : varname) (T1 T2 : type) (t1 : term),
         has_type (M.add x T1 Γ) t1 T2 ->
         has_type Γ (term_abs x T1 t1) (type_Arrow T1 T2)
 
@@ -510,13 +606,13 @@ Module Chap11.
 
     | T_Wildcard : forall (Γ : context) (t : term) (T : type),
         has_type Γ t T ->
-        has_type Γ (term_abs "_" T t) (type_Arrow T type_Unit)
+        has_type Γ (term_abs varname_unused T t) (type_Arrow T type_Unit)
 
     | T_Ascribe : forall (Γ : context) (t : term) (T : type),
         has_type Γ t T ->
         has_type Γ (term_ascribe t T) T
 
-    | T_Let : forall (Γ : context) (x : string) (t1 t2 : term) (T1 T2 : type),
+    | T_Let : forall (Γ : context) (x : varname) (t1 t2 : term) (T1 T2 : type),
         has_type Γ t1 T1 ->
         has_type (M.add x T1 Γ) t2 T2 ->
         has_type Γ (term_let x t1 t2) T2
@@ -534,7 +630,7 @@ Module Chap11.
         has_type Γ (term_snd t) T2
 
     | T_Tuple : forall (Γ : context) (ts : list term) (Ts : list type),
-        (forall t T, In (t, T) (combine ts Ts) -> has_type Γ t T) ->
+        Forall2 (has_type Γ) ts Ts ->
         has_type Γ (term_tuple ts) (type_Tuple Ts)
     | T_TupleProj : forall (Γ : context) (t : term) (Ts : list type) (n : nat) (T : type),
         has_type Γ t (type_Tuple Ts) ->
@@ -543,9 +639,7 @@ Module Chap11.
         has_type Γ (term_tuple_proj t n) T
 
     | T_Rcd : forall (Γ : context) (m : list (record_label * term)) (Ts : list type),
-        (forall (k : record_label) (v : term) (T : type),
-          In (k, T) (combine (map fst m) Ts) ->
-          has_type Γ v T) ->
+        Forall2 (has_type Γ) (map snd m) Ts ->
         has_type Γ (term_record m) (type_Record (combine (map fst m) Ts))
     | T_RcdProj : forall (Γ : context) (t : term) (m : list (record_label * type)) (k : record_label) (T : type),
         has_type Γ t (type_Record m) ->
@@ -558,7 +652,7 @@ Module Chap11.
     | T_Inr : forall (Γ : context) (t : term) (T1 T2 : type),
         has_type Γ t T2 ->
         has_type Γ (term_inr t (type_Sum T1 T2)) (type_Sum T1 T2)
-    | T_Case : forall (Γ : context) (t0 t1 t2 : term) (x1 x2 : string) (T1 T2 T : type),
+    | T_Case : forall (Γ : context) (t0 t1 t2 : term) (x1 x2 : varname) (T1 T2 T : type),
         has_type Γ t0 (type_Sum T1 T2) ->
         has_type (M.add x1 T1 Γ) t1 T ->
         has_type (M.add x2 T2 Γ) t2 T ->
@@ -582,31 +676,289 @@ Module Chap11.
 
     | T_Fix : forall (Γ : context) (t1 : term) (T1 : type),
         has_type Γ t1 (type_Arrow T1 T1) ->
-        has_type Γ (term_fix t1) T1.
+        has_type Γ (term_fix t1) T1
 
-  (* 11.3.2 *)
-  (* Give typing and evaluation rules for wildcard abstractions, and
-     prove that they can be derived from the abbreviation stated above. *)
+    | T_Nil : forall (Γ : context) (T : type),
+        has_type Γ (term_nil T) (type_List T)
+    | T_Cons : forall (Γ : context) (t1 t2 : term) (T : type),
+        has_type Γ t1 T ->
+        has_type Γ t2 (type_List T) ->
+        has_type Γ (term_cons T t1 t2) (type_List T)
+    | T_IsNil : forall (Γ : context) (t : term) (T : type),
+        has_type Γ t (type_List T) ->
+        has_type Γ (term_is_nil T t) type_Bool
+    | T_Head : forall (Γ : context) (t : term) (T : type),
+        has_type Γ t (type_List T) ->
+        has_type Γ (term_head T t) T
+    | T_Tail : forall (Γ : context) (t : term) (T : type),
+        has_type Γ t (type_List T) ->
+        has_type Γ (term_tail T t) (type_List T).
 
-  (* Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
+  (* NOTE: we have proved these in previous chapters, but they are getting cumbersome
+           to prove with so much stuff around, so we will just assume them for now. *)
+
+  Lemma nth_skipn : forall (A : Type) (l : list A) (n : nat) (d : A),
+    n < length l ->
+    nth n l d :: skipn (S n) l = skipn n l.
+  Proof.
+    intros A l n d Hlen.
+    revert n Hlen.
+    induction l as [| h l IH]; intros n Hlen.
+    - inversion Hlen.
+    - destruct n.
+      + simpl. reflexivity.
+      + apply IH.
+        rewrite length_cons in Hlen.
+        rewrite <- Nat.succ_lt_mono in Hlen.
+        assumption.
+  Qed.
+
+  Lemma firstn_nth_skipn : forall (A : Type) (l : list A) (n : nat) (d : A),
+    n < length l ->
+    List.app (firstn n l) (nth n l d :: skipn (S n) l) = l.
+  Proof.
+    intros A l n d Hlen.
+    rewrite nth_skipn with (d := d) (l := l) (n := n).
+    - rewrite firstn_skipn with (l := l) (n := n).
+      reflexivity.
+    - assumption.
+  Qed.
+
+  Lemma step_value_stuck : forall (t t' : term),
+    is_value t ->
+    step t t' ->
+    t = t'.
+  Proof.
+    intros t t' Hval Hstep.
+    induction Hstep.
+    all: (
+      try (inversion Hval; subst; auto);
+      try (intuition eauto; subst; reflexivity)
+    ).
+    - assert (In (nth j t term_unit) t) as tj_in_t. {
+        apply nth_In.
+        assumption.
+      }
+      pose proof (H3 (nth j t term_unit) tj_in_t) as Htj_val.
+      specialize (IHHstep Htj_val). subst.
+      assert (t = t') as Htuple_eq. {
+        rewrite <- firstn_nth_skipn with (n := j) (l := t) (d := term_unit).
+        - reflexivity.
+        - assumption.
+      }
+      rewrite Htuple_eq.
+      reflexivity.
+    - assert (In (nth j r ("", term_unit)) r) as tj_in_r. {
+        apply nth_In.
+        assumption.
+      }
+      assert (is_value (snd (nth j r ("", term_unit)))) as Htj_val. {
+        apply (H3 (fst (nth j r ("", term_unit))) (snd (nth j r ("", term_unit)))).
+        rewrite <- surjective_pairing.
+        assumption.
+      }
+      specialize (IHHstep Htj_val). subst.
+      assert (r = r') as Hrcd_eq. {
+        rewrite <- firstn_nth_skipn with (n := j) (l := r) (d := ("", term_unit)).
+        - reflexivity.
+        - assumption.
+      }
+      rewrite Hrcd_eq.
+      reflexivity.
+  Qed.
+
+  Lemma step_deterministic : forall (t t1 t2 : term),
+    step t t1 -> step t t2 -> t1 = t2.
+  Proof.
+    intros t t1' t2' Hstep.
+    generalize dependent t2'.
+    (* induction on the derivation of (t -> t1') *)
+    induction Hstep.
+    all: (
+      intros t2'' Hstep2;
+      try (inversion Hstep2; subst; apply IHHstep in H2; subst; reflexivity);
+      try (inversion Hstep2; subst; apply IHHstep in H3; subst; reflexivity)
+    ).
+  Admitted.
+
+  Lemma uniqueness_of_types : forall (Γ : context) (t : term) (T1 T2 : type),
+    has_type Γ t T1 -> has_type Γ t T2 -> T1 = T2.
+  Proof. Admitted.
+
+  Lemma canonical_forms_bool : forall (Γ : context) (t : term) (T : type),
+    is_value t ->
+    has_type Γ t type_Bool ->
+    t = term_true \/ t = term_false.
+  Proof.
+    intros Γ t T Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+  Qed.
+
+  Lemma canonical_forms_unit : forall (Γ : context) (t : term) (T : type),
+    is_value t ->
+    has_type Γ t type_Unit ->
+    t = term_unit.
+  Proof.
+    intros Γ t T Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+  Qed.
+
+  Lemma canonical_forms_arrow : forall (Γ : context) (t : term) (T1 T2 : type),
+    is_value t ->
+    has_type Γ t (type_Arrow T1 T2) ->
+    exists x t1, t = term_abs x T1 t1.
+  Proof.
+    intros Γ t T1 T2 Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    - exists x, t1.
+      reflexivity.
+    - exists varname_unused, t0.
+      reflexivity.
+  Qed.
+
+  Lemma canonical_forms_product : forall (Γ : context) (t : term) (T1 T2 : type),
+    is_value t ->
+    has_type Γ t (type_Product T1 T2) ->
+    exists v1 v2, t = term_pair v1 v2 /\ is_value v1 /\ is_value v2.
+  Proof.
+    intros Γ t T1 T2 Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    exists t1, t2.
+    split; [reflexivity | split; assumption].
+  Qed.
+
+  Lemma canonical_forms_sum : forall (Γ : context) (t : term) (T1 T2 : type),
+    is_value t ->
+    has_type Γ t (type_Sum T1 T2) ->
+    (exists v, t = term_inl v (type_Sum T1 T2) /\ is_value v) \/
+    (exists v, t = term_inr v (type_Sum T1 T2) /\ is_value v).
+  Proof.
+    intros Γ t T1 T2 Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    - left. exists t0. split; [reflexivity | assumption].
+    - right. exists t0. split; [reflexivity | assumption].
+  Qed.
+
+  Lemma canonical_forms_variant : forall (Γ : context) (t : term) (c : list (record_label * type)),
+    is_value t ->
+    has_type Γ t (type_Variant c) ->
+    exists (l : record_label) (v : term) (T : type),
+      In (l, T) c /\
+      t = term_variant l v (type_Variant c) /\
+      is_value v.
+  Proof.
+    intros Γ t c Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    exists l, tj, Tj.
+    split; [assumption | split; [reflexivity | assumption]].
+  Qed.
+
+  Lemma canonical_forms_tuple : forall (Γ : context) (t : term) (Ts : list type),
+    is_value t ->
+    has_type Γ t (type_Tuple Ts) ->
+    exists vs, t = term_tuple vs /\ length vs = length Ts /\ (forall v, In v vs -> is_value v).
+  Proof.
+    intros Γ t Ts Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    exists ts.
+    split.
+    reflexivity.
+    split.
+    - apply Forall2_length in H2.
+      assumption.
+    - assumption.
+  Qed.
+
+  Lemma canonical_forms_record : forall (Γ : context) (t : term) (m : list (record_label * type)),
+    is_value t ->
+    has_type Γ t (type_Record m) ->
+    exists vs, t = term_record vs /\ length vs = length m /\ (forall k v, In (k, v) vs -> is_value v).
+  Proof.
+    intros Γ t m Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    exists m0.
+    split.
+    reflexivity.
+    split.
+    - apply Forall2_length in H2.
+      rewrite length_combine.
+      rewrite length_map.
+      rewrite <- H2.
+      rewrite length_map.
+      rewrite Nat.min_id.
+      reflexivity.
+    - assumption.
+  Qed.
+
+  Lemma canonical_forms_list : forall (Γ : context) (t : term) (T : type),
+    is_value t ->
+    has_type Γ t (type_List T) ->
+    (t = term_nil T) \/ (exists v1 v2, t = term_cons T v1 v2 /\ is_value v1 /\ is_value v2).
+  Proof.
+    intros Γ t T Hval Htyp.
+    inversion Htyp; subst; try (inversion Hval; subst; auto).
+    right.
+    exists t1, t2.
+    split; [reflexivity | split; assumption].
+  Qed.
+
+  Lemma progress : forall (Γ : context) (t : term) (T : type),
+    has_type Γ t T ->
+    is_value t \/ exists t', step t t'.
+  Proof. Admitted.
+
+  Lemma preservation : forall (Γ : context) (t t' : term) (T : type),
+    has_type Γ t T ->
+    step t t' ->
+    has_type Γ t' T.
+  Proof. Admitted.
+
+  Lemma subst_noop_ih : forall (x : varname) (v t t' : term),
+    (~ is_free_variable x t -> substitute x v t = t) ->
+    ~ is_free_variable x t' ->
+    (is_free_variable x t -> is_free_variable x t') ->
+    substitute x v t = t.
+  Proof.
+    intros x v t t' IH Hfv Cons.
+    apply IH.
+    intros Hfv'.
+    apply Hfv.
+    apply Cons.
+    exact Hfv'.
+  Qed.
+
+  Lemma substitution_noop : forall (Γ : context) (x : varname) (v t : term) (T : type),
     ~ is_free_variable x t ->
       substitute x v t = t.
   Proof.
     intros Γ x v t T Hfv.
-    induction t; simpl in *; try reflexivity.
-    - destruct (String.eqb_spec x s) as [Heq | Hneq].
+    induction t.
+    all: (
+      (* Takes care of values *)
+      try (simpl; reflexivity)
+    ).
+
+    (* term_var *)
+    - destruct (varname_eq_dec x v0) as [Heq | Hneq].
       + subst.
         exfalso.
         apply Hfv.
-        apply FV_Var.
-      + reflexivity.
-    - assert (substitute x v t1 = t1) as Hsub1.
-      { apply IHt1. intros Hfv'. apply Hfv. apply FV_App1. exact Hfv'. }
-      assert (substitute x v t2 = t2) as Hsub2.
-      { apply IHt2. intros Hfv'. apply Hfv. apply FV_App2. exact Hfv'. }
-      rewrite Hsub1, Hsub2.
-      reflexivity.
-    - destruct (String.eqb_spec x s) as [Heq | Hneq].
+        constructor.
+      + unfold substitute.
+        apply varname_eqb_neq in Hneq.
+        rewrite Hneq.
+        reflexivity.
+
+    (* term_app *)
+    - pose proof (subst_noop_ih _ _ _ _ IHt1 Hfv (FV_App1 _ _ _)) as Hsub1.
+      pose proof (subst_noop_ih _ _ _ _ IHt2 Hfv (FV_App2 _ _ _)) as Hsub2.
+      rewrite <- Hsub1 at 2.
+      rewrite <- Hsub2 at 2.
+      constructor.
+
+    (* term_abs *)
+    - simpl.
+      destruct (varname_eqb_spec x v0) as [Heq | Hneq].
       + subst.
         reflexivity.
       + assert (substitute x v t0 = t0) as Hsub.
@@ -621,43 +973,62 @@ Module Chap11.
         }
         rewrite Hsub.
         reflexivity.
-    - assert (substitute x v t1 = t1) as Hsub1.
-      { apply IHt1. intros Hfv'. apply Hfv. apply FV_If1. exact Hfv'. }
-      assert (substitute x v t2 = t2) as Hsub2.
-      { apply IHt2. intros Hfv'. apply Hfv. apply FV_If2. exact Hfv'. }
-      assert (substitute x v t3 = t3) as Hsub3.
-      { apply IHt3. intros Hfv'. apply Hfv. apply FV_If3. exact Hfv'. }
+
+    (* term_if *)
+    - simpl.
+      pose proof (subst_noop_ih _ _ _ _ IHt1 Hfv (FV_If1 _ _ _ _)) as Hsub1.
+      pose proof (subst_noop_ih _ _ _ _ IHt2 Hfv (FV_If2 _ _ _ _)) as Hsub2.
+      pose proof (subst_noop_ih _ _ _ _ IHt3 Hfv (FV_If3 _ _ _ _)) as Hsub3.
       rewrite Hsub1, Hsub2, Hsub3.
       reflexivity.
-    - assert (substitute x v t = t) as Hsub.
-      { apply IHt. intros Hfv'. apply Hfv. apply FV_Ascribe. exact Hfv'. }
-      rewrite Hsub.
-      reflexivity.
-  Qed.
 
-  Lemma substitution_preserves_typing : forall (Γ : context) (x : string) (v t : term) (T1 T2 : type),
+    (* term_ascribe *)
+    - pose proof (subst_noop_ih _ _ _ _ IHt Hfv (FV_Ascribe _ _ _)) as Hsub.
+      rewrite <- Hsub at 2.
+      reflexivity.
+
+    (* term_let *)
+    - destruct (varname_eqb_spec x v0) as [Heq | Hneq].
+  Admitted.
+
+  Lemma substitution_preserves_typing : forall (Γ : context) (x : varname) (v t : term) (T1 T2 : type),
       has_type (M.add x T2 Γ) t T1 ->
       has_type Γ v T2 ->
       has_type Γ (substitute x v t) T1.
-  Proof.
-    intros Γ x v t T1 T2 Ht Hv.
-    generalize dependent Γ.
-    generalize dependent T1.
-    induction t; intros T1 Γ Ht; simpl in *; inversion Ht; subst; try (econstructor; eauto). *)
+  Proof. Admitted.
 
-  Definition wildcard (t : term) (T : type) : term :=
-    term_app (term_abs "_" T t) (term_unit).
+  (* Lemma step_fv_app_abs : forall (Γ : context) (x : varname) (v t : term) (T : type),
+    is_value v ->
+    ~ is_free_variable x t ->
+    step (term_app (term_abs x T t) v) v.
+  Proof.
+    intros Γ x v t T Hval Hfv.
+    assert (substitute x v t = v) as Hsub.
+    {
+      apply substitution_noop.
+      assumption.
+      assumption.
+      exact Hfv.
+    }
+    apply E_AppAbs.
+    rewrite <- Hsub at 2. *)
+
+  (* 11.3.2 *)
+  (* Give typing and evaluation rules for wildcard abstractions, and
+     prove that they can be derived from the abbreviation stated above. *)
+
+  Definition term_wildcard (t : term) (T : type) : term :=
+    term_abs varname_unused T t.
 
   Lemma wildcard_typing : forall Γ t T,
-    has_type Γ (wildcard t T) (type_Arrow T type_Unit).
-  Proof.
-  Admitted.
+    has_type Γ (term_wildcard t T) (type_Arrow T T).
+  Proof. Admitted.
 
   Lemma wildcard_evaluation : forall t T,
-    step (wildcard t T) t.
+    step (term_wildcard t T) t.
   Proof.
     intros t T.
-    unfold wildcard.
+    unfold term_wildcard.
   Admitted.
 
   (* 11.4.1 (1) *)
@@ -665,7 +1036,8 @@ Module Chap11.
      Prove that the “official” typing and evaluation rules given here
      correspond to your definition in a suitable sense. *)
   Definition ascribe' (t : term) (T : type) : term :=
-    term_app (term_abs "x" T (term_var "x")) (t).
+    let x := fresh_varname (varnames t) in
+    term_app (term_abs x T (term_var x)) (t).
 
   Lemma ascribe'_typing : forall Γ t T,
     has_type Γ (ascribe' t T) T <-> has_type Γ t T.
@@ -682,6 +1054,6 @@ Module Chap11.
         apply T_Var.
         apply MFacts.add_eq_o.
         reflexivity.
-      + exact H.
+     + exact H.
   Qed.
 End Chap11.
\ No newline at end of file