diff --git a/src/chap11.v b/src/chap11.v
index 54e3c30..4982e4e 100644
--- a/src/chap11.v
+++ b/src/chap11.v
@@ -22,32 +22,86 @@ Module Chap11.
   *)
 
   Definition varname := string.
+  Definition record_label := string.
 
   Inductive type : Type :=
+    (** T1 -> T2 *)
     | type_Arrow : type -> type -> type
+    (** ArbitraryType *)
     | type_Base : string -> type
+    (** T1 x T2 *)
     | type_Product : type -> type -> type
-    | type_Tuple : list type -> type.
-
+    (** {T1, T2, ..., Tn} *)
+    | type_Tuple : list type -> type
+    (** { k1 : T1, k2 : T2, ..., kn : Tn } *)
+    | type_Record : list (record_label * type) -> type
+    (** T1 + T2 *)
+    | type_Sum : type -> type -> type
+    (** <l1 : T1, l2 : T2, ..., ln : Tn> *)
+    | type_Variant : list (record_label * 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.
+  Definition context := M.t type.
+  Definition empty_ctx : context := @M.empty type.
+
   Inductive term : Type :=
+    (** x *)
     | term_var : varname -> term
+    (** t1 t2 *)
     | term_app : term -> term -> term
+    (** (λx:T. t) *)
     | term_abs : varname -> type -> term -> term
+    (** true *)
     | term_true : term
+    (** false *)
     | term_false : term
+    (** if t1 then t2 else t3 *)
     | term_if : term -> term -> term -> term
+    (** unit *)
     | term_unit : term
+    (** t as T *)
     | term_ascribe : term -> type -> term
+    (** let x = t1 in t2 *)
     | term_let : varname -> term -> term -> term
+
+    (** {1,2} *)
     | term_pair : term -> term -> term
+    (** fst {1,2} *)
     | term_fst : term -> term
+    (** snd {1,2} *)
     | term_snd : term -> term
+
+    (** {5, true} *)
     | term_tuple : list term -> term
-    | term_tuple_proj : term -> nat -> term.
+    (** {5, true}.1 *)
+    | term_tuple_proj : term -> nat -> term
+
+    (** { k = 1, y = true } *)
+    | term_record : list (record_label * term) -> term
+    (** { k = 1, y = true }.k *)
+    | term_record_proj : term -> record_label -> term
+    (** let p = t1 in t2 *)
+    | term_pattern_bind : term -> term -> term -> term
+
+    (** inl t as T *)
+    | term_inl : term -> type -> term
+    (** inr t as T*)
+    | term_inr : term -> type -> term
+    (** case (t as T) of inl x => t1 | inr y => t2 *)
+    | term_case : term -> type -> varname -> term -> varname -> term -> term
+
+    (** <var=t> as T *)
+    | term_variant : record_label -> term -> type -> term
+
+    (** case t of <l_i=x_i> => t_i *)
+    | term_variant_case : term -> list (record_label * varname * term) -> term
+
+    (** fix t *)
+    | term_fix : 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
@@ -55,27 +109,44 @@ Module Chap11.
   Definition term_seq (t1 t2 : term) : term :=
     term_app (term_abs "_" type_Unit t2) t1.
 
-  Module M := FMapList.Make(String_as_OT).
-  Module MFacts := FMapFacts.WFacts_fun String_as_OT M.
-  Definition context := M.t type.
-  Definition empty_ctx : context := @M.empty type.
+  Definition term_letrec (x : string) (T1 : type) (t1 : term) (t2 : term) : term :=
+    term_let x (term_fix (term_abs x T1 t1)) t2.
 
-  Inductive value : term -> Prop :=
+  Inductive is_value : term -> Prop :=
     | v_abs : forall (x : string) (T2 : type) (t1 : term),
-        value (term_abs x T2 t1)
+        is_value (term_abs x T2 t1)
     | v_true :
-        value term_true
+        is_value term_true
     | v_false :
-        value term_false
+        is_value term_false
     | v_unit :
-        value term_unit
+        is_value term_unit
     | v_pair : forall (v1 v2 : term),
-        value v1 ->
-        value v2 ->
-        value (term_pair v1 v2)
+        is_value v1 ->
+        is_value v2 ->
+        is_value (term_pair v1 v2)
     | v_tuple : forall (vs : list term),
-        (forall v, In v vs -> value v) ->
-        value (term_tuple vs).
+        (forall v, In v vs -> is_value v) ->
+        is_value (term_tuple vs)
+    | v_record : forall (m : list (record_label * term)),
+        (forall k v, In (k, v) m -> is_value v) ->
+        is_value (term_record m)
+    | v_inl : forall (v : term) (T : type),
+        is_value v ->
+        is_value (term_inl v T)
+    | v_inr : forall (v : term) (T : type),
+        is_value v ->
+        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).
+
+  Inductive is_pattern : term -> Prop :=
+    | p_var : forall (x : string),
+        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
@@ -139,7 +210,15 @@ Module Chap11.
         is_free_variable x (term_tuple ts)
     | FV_TupleProj : forall x t n,
         is_free_variable x t ->
-        is_free_variable x (term_tuple_proj t n).
+        is_free_variable x (term_tuple_proj t n)
+
+    | FV_Record : forall x m,
+        (forall k v, In (k, v) m -> is_free_variable x v) ->
+        is_free_variable x (term_record m)
+    | FV_RecordProj : forall x t k,
+        is_free_variable x t ->
+        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
@@ -205,6 +284,7 @@ Module Chap11.
 
 
   Fixpoint substitute (x : string) (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
@@ -213,108 +293,192 @@ Module Chap11.
     | term_abs y T t1 =>
         if String.eqb x y
           then t
-          else term_abs y T (substitute x s t1)
-    | term_app t1 t2 =>
-        term_app (substitute x s t1) (substitute x s t2)
-    | term_true =>
-        term_true
-    | term_false =>
-        term_false
-    | term_unit =>
-        term_unit
-    | term_if t1 t2 t3 =>
-        term_if (substitute x s t1) (substitute x s t2) (substitute x s t3)
-    | term_ascribe t1 T =>
-        term_ascribe (substitute x s t1) T
+          else term_abs y T (f t1)
+    | term_app t1 t2 => term_app (f t1) (f t2)
+    | term_true => term_true
+    | term_false =>  term_false
+    | term_unit => term_unit
+    | 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
-          then term_let y (substitute x s t1) t2
-          else term_let y (substitute x s t1) (substitute x s t2)
-    | term_pair t1 t2 =>
-        term_pair (substitute x s t1) (substitute x s t2)
-    | term_fst t1 =>
-        term_fst (substitute x s t1)
-    | term_snd t1 =>
-        term_snd (substitute x s t1)
-    | term_tuple ts =>
-        term_tuple (map (substitute x s) ts)
-    | term_tuple_proj t n =>
-        term_tuple_proj (substitute x s t) n
+          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)
+    | term_fst t1 => term_fst (f t1)
+    | term_snd t1 => term_snd (f t1)
+    | term_tuple ts => term_tuple (map f ts)
+    | term_tuple_proj t n => term_tuple_proj (f t) n
+    | term_record m => term_record (map (fun '(k, v) => (k, f v)) m)
+    | term_record_proj t k => term_record_proj (f t) k
+    | term_pattern_bind p t1 t2 => term_pattern_bind p (f t1) (f t2)
+    | term_inl t1 T => term_inl (f t1) T
+    | term_inr t1 T => term_inr (f t1) T
+    | term_case t0 T x t1 y t2 => term_case (f t0) T x (f t1) y (f t2)
+    | term_variant l t1 T => term_variant l (f t1) T
+    | 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)
     end.
 
+  Inductive matching : term -> term -> term -> Prop :=
+    (** match(x, 5) -> [x -> 5] *)
+    | M_Var : forall (x : string) (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]
+        match(x, {5, true}) -> [x -> {5, true}]  *)
+    (* | M_Rcd : forall (t :  *)
+
   Inductive step : term -> term -> Prop :=
-    | E_App1 : forall t1 t1' t2,
+    | E_App1 : forall (t1 t1' t2 : term),
           step t1 t1' ->
           step (term_app t1 t2) (term_app t1' t2)
-    | E_App2 : forall v1 t2 t2',
-          value v1 ->
+    | E_App2 : forall (v1 t2 t2' : term),
+          is_value v1 ->
           step t2 t2' ->
           step (term_app v1 t2) (term_app v1 t2')
 
-    | E_AppAbs : forall x T t v,
-          value v ->
+    | E_AppAbs : forall (x : string) (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,
+    | E_Wildcard : forall (t1 t2 : term),
           step (term_app (term_abs "_" type_Unit t1) t2) t1
 
-    | E_IfTrue : forall t1 t2,
+    | E_IfTrue : forall (t1 t2 : term),
         step (term_if term_true t1 t2) t1
-    | E_IfFalse : forall t1 t2,
+    | E_IfFalse : forall (t1 t2 : term),
         step (term_if term_false t1 t2) t2
-    | E_If : forall t1 t1' t2 t3,
+    | E_If : forall (t1 t1' t2 t3 : term),
         step t1 t1' ->
         step (term_if t1 t2 t3) (term_if t1' t2 t3)
 
-    | E_Ascribe : forall v T,
-        value v ->
+    | E_Ascribe : forall (v : term) (T : type),
+        is_value v ->
         step (term_ascribe v T) v
-    | E_Ascribe1 : forall t t' T,
+    | E_Ascribe1 : forall (t t' : term) (T : type),
         step t t' ->
         step (term_ascribe t T) (term_ascribe t' T)
 
-    | E_LetV : forall x v t2,
-        value v ->
+    | E_LetV : forall (x : string) (v t2 : term),
+        is_value v ->
         step (term_let x v t2) (substitute x v t2)
-    | E_Let : forall x t1 t1' t2,
+    | E_Let : forall (x : string) (t1 t1' t2 : term),
         step t1 t1' ->
         step (term_let x t1 t2) (term_let x t1' t2)
 
-    | E_PairBeta1 : forall v1 v2,
-        value v1 ->
-        value v2 ->
+    | E_PairBeta1 : forall (v1 v2 : term),
+        is_value v1 ->
+        is_value v2 ->
         step (term_fst (term_pair v1 v2)) v1
-    | E_PairBeta2 : forall v1 v2,
-        value v1 ->
-        value v2 ->
+    | E_PairBeta2 : forall (v1 v2 : term),
+        is_value v1 ->
+        is_value v2 ->
         step (term_snd (term_pair v1 v2)) v2
-    | E_Proj1 : forall t1 t1',
+    | E_Proj1 : forall (t1 t1' : term),
         step t1 t1' ->
         step (term_fst t1) (term_fst t1')
-    | E_Proj2 : forall t1 t1',
+    | E_Proj2 : forall (t1 t1' : term),
         step t1 t1' ->
         step (term_snd t1) (term_snd t1')
-    | E_Pair1 : forall t1 t1' t2,
+    | E_Pair1 : forall (t1 t1' t2 : term),
         step t1 t1' ->
         step (term_pair t1 t2) (term_pair t1' t2)
-    | E_Pair2 : forall v1 t2 t2',
-        value v1 ->
+    | E_Pair2 : forall (v1 t2 t2' : term),
+        is_value v1 ->
         step t2 t2' ->
         step (term_pair v1 t2) (term_pair v1 t2')
 
     | E_ProjTuple :
-        forall vs n,
-          (forall v, In v vs -> value v) ->
+        forall (vs : list term) (n : nat),
+          (forall v, In v vs -> is_value v) ->
           n < length vs ->
           step (term_tuple_proj (term_tuple vs) n) (nth n vs term_unit)
-    | E_Proj : forall t1 t1' n,
+    | E_Proj : forall (t1 t1' : term) (n : nat),
         step t1 t1' ->
         step (term_tuple_proj t1 n) (term_tuple_proj t1' n)
-    | E_Tuple : forall ts ts' n,
-        (forall i, i < n -> i < length ts -> value (nth i ts term_unit)) ->
-        (step (nth n ts term_unit) (nth n ts' term_unit)) ->
-        ts' = List.app (firstn n ts) ((nth n ts' term_unit) :: (skipn (S n) ts)) ->
-        step (term_tuple ts) (term_tuple ts').
+    | E_Tuple : forall (t : list term) (tj tj' : term) (j : nat),
+        (* j is bounded by the length of the tuple *)
+        0 <= j < length t ->
+        (* All terms before j are values *)
+        (forall i,
+          1 <= i < j ->
+          i < length t ->
+          is_value (nth i t term_unit)) ->
+        (* 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
+        step (term_tuple t) (term_tuple t')
+
+    | E_ProjRcd : forall (k : record_label) (v : term) (m : list (record_label * term)),
+        (forall k' v', In (k', v') m -> is_value v') ->
+        In (k, v) m ->
+        step (term_record_proj (term_record m) k) v
+    | 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),
+        (* j is bounded by the length of the record *)
+        1 <= 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)))) ->
+        (* j-th element is an evaluatable term *)
+        tj = snd (nth j r ("", term_unit)) ->
+        step tj tj' ->
+        (* r' is the record with the j-th element replaced by tj' *)
+        let r' := List.app (firstn j r) (nth j r ("", term_unit) :: (skipn (S j) r)) in
+        step (term_record r) (term_record r')
+
+    (* TODO: this should possibly perform some sort of substitution *)
+    | E_LetVPattern : forall (p v t2 : term),
+        is_pattern p ->
+        is_value v ->
+        matching p v t2 ->
+        step (term_pattern_bind p v t2) t2
+
+    | E_LetPattern : forall (p t1 t1' t2 : term),
+        is_pattern p ->
+        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),
+        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),
+        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),
+        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),
+        step t t' ->
+        step (term_inl t T) (term_inl t' T)
+    | E_Inr : forall (t t' : term) (T : type),
+        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)),
+        is_value vj ->
+        In (lj, xj, tj) c ->
+        step (term_variant_case (term_variant lj vj T) c) (substitute xj vj tj)
+    | E_Case' : forall (t0 t0' : term) (c : list (record_label * varname * term)),
+        step t0 t0' ->
+        step (term_variant_case t0 c) (term_variant_case t0' c)
+    | E_Variant : forall (l : record_label) (t t' : term) (T : type),
+        step t t' ->
+        step (term_variant l t T) (term_variant l t' T)
+
+    | E_FixBeta : forall (x : string) (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').
 
   Inductive has_type : context -> term -> type -> Prop :=
     | T_Var : forall (Γ : context) (x : string) (T1 : type),
@@ -330,59 +494,101 @@ Module Chap11.
         has_type Γ t2 T2 ->
         has_type Γ (term_app t1 t2) T1
 
-    | T_True : forall Γ,
+    | T_True : forall (Γ : context),
         has_type Γ term_true type_Bool
-    | T_False : forall Γ,
+    | T_False : forall (Γ : context),
         has_type Γ term_false type_Bool
 
-    | T_If : forall t1 t2 t3 T1 Γ,
+    | T_If : forall (Γ : context) (t1 t2 t3 : term) (T1 : type),
         has_type Γ t1 type_Bool ->
         has_type Γ t2 T1 ->
         has_type Γ t3 T1 ->
         has_type Γ (term_if t1 t2 t3) T1
 
-    | T_Unit : forall Γ,
+    | T_Unit : forall (Γ : context),
         has_type Γ term_unit type_Unit
 
-    | T_Wildcard : forall Γ t T,
+    | T_Wildcard : forall (Γ : context) (t : term) (T : type),
         has_type Γ t T ->
         has_type Γ (term_abs "_" T t) (type_Arrow T type_Unit)
 
-    | T_Ascribe : forall Γ t T,
+    | T_Ascribe : forall (Γ : context) (t : term) (T : type),
         has_type Γ t T ->
         has_type Γ (term_ascribe t T) T
 
-    | T_Let : forall Γ x t1 t2 T1 T2,
+    | T_Let : forall (Γ : context) (x : string) (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
 
-    | T_Pair : forall Γ t1 t2 T1 T2,
+    | T_Pair : forall (Γ : context) (t1 t2 : term) (T1 T2 : type),
         has_type Γ t1 T1 ->
         has_type Γ t2 T2 ->
         has_type Γ (term_pair t1 t2) (type_Product T1 T2)
 
-    | T_Proj1 : forall Γ t T1 T2,
+    | T_Proj1 : forall (Γ : context) (t : term) (T1 T2 : type),
         has_type Γ t (type_Product T1 T2) ->
         has_type Γ (term_fst t) T1
-    | T_Proj2 : forall Γ t T1 T2,
+    | T_Proj2 : forall (Γ : context) (t : term) (T1 T2 : type),
         has_type Γ t (type_Product T1 T2) ->
         has_type Γ (term_snd t) T2
 
-    | T_Tuple : forall Γ ts Ts,
+    | T_Tuple : forall (Γ : context) (ts : list term) (Ts : list type),
         (forall t T, In (t, T) (combine ts Ts) -> has_type Γ t T) ->
         has_type Γ (term_tuple ts) (type_Tuple Ts)
-    | T_Proj : forall Γ t Ts n T,
+    | T_TupleProj : forall (Γ : context) (t : term) (Ts : list type) (n : nat) (T : type),
         has_type Γ t (type_Tuple Ts) ->
         n < length Ts ->
         nth_error Ts n = Some T ->
-        has_type Γ (term_tuple_proj t n) T.
+        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) ->
+        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) ->
+        In (k, T) m ->
+        has_type Γ (term_record_proj t k) T
+
+    | T_Inl : forall (Γ : context) (t : term) (T1 T2 : type),
+        has_type Γ t T1 ->
+        has_type Γ (term_inl t (type_Sum T1 T2)) (type_Sum T1 T2)
+    | 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),
+        has_type Γ t0 (type_Sum T1 T2) ->
+        has_type (M.add x1 T1 Γ) t1 T ->
+        has_type (M.add x2 T2 Γ) t2 T ->
+        has_type Γ (term_case t0 T x1 t1 x2 t2) T
+
+    | T_Variant : forall (Γ : context) (tj : term) (l : record_label) (Tj : type) (c : list (record_label * type)),
+        has_type Γ tj Tj ->
+        In (l, Tj) c ->
+        has_type Γ (term_variant l tj (type_Variant c)) (type_Variant c)
+    | T_VariantCase : forall (Γ : context) (t0 : term) (cs : list (record_label * varname * term)) (Ts: list (record_label * type)) (T : type),
+        (* All labels in the case must be in the type *)
+        let case_labels := map (fun '(l, _, _) => l) cs in
+        let type_labels := map (fun '(l, _) => l) Ts in
+        (forall l, In l case_labels <-> In l type_labels) ->
+        (* All types in the typemap must yield T for the entire variant *)
+        (forall (l : record_label) (x : varname) (t : term) (T' : type),
+          In (l, x, t) cs ->
+          In (l, T') Ts ->
+          has_type (M.add x T' Γ) t T) ->
+        has_type Γ (term_variant_case t0 cs) T
+
+    | T_Fix : forall (Γ : context) (t1 : term) (T1 : type),
+        has_type Γ t1 (type_Arrow 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. *)
 
-  Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
+  (* Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
     ~ is_free_variable x t ->
       substitute x v t = t.
   Proof.
@@ -437,7 +643,7 @@ Module Chap11.
     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).
+    induction t; intros T1 Γ Ht; simpl in *; inversion Ht; subst; try (econstructor; eauto). *)
 
   Definition wildcard (t : term) (T : type) : term :=
     term_app (term_abs "_" T t) (term_unit).