diff --git a/src/chap8.v b/src/chap8.v
new file mode 100644
index 0000000..e839907
--- /dev/null
+++ b/src/chap8.v
@@ -0,0 +1,627 @@
+
+Module Chap8.
+  (* 8.1 *)
+  Inductive term : Type :=
+  | ttrue
+  | tfalse
+  | iif (t1 t2 t3 : term)
+  | O
+  | succ (t : term)
+  | pred (t : term)
+  | iszero (t : term).
+
+  Scheme Equality for term.
+
+  Inductive is_numeric_val : term -> Prop :=
+  | nv_O : is_numeric_val O
+  | nv_succ : forall t, is_numeric_val t -> is_numeric_val (succ t).
+
+  Inductive is_value : term -> Prop :=
+  | v_true : is_value ttrue
+  | v_false : is_value tfalse
+  | v_num : forall t, is_numeric_val t -> is_value t.
+
+  Lemma numeric_value_is_value : forall (t : term),
+    is_numeric_val t -> is_value t.
+  Proof.
+    intros t H.
+    destruct H as [| t' H'].
+    - apply v_num. exact nv_O.
+    - apply v_num. apply nv_succ. exact H'.
+  Qed.
+
+  (* 8.2 *)
+  Inductive type : Type :=
+  | TBool
+  | TNat.
+
+  Scheme Equality for type.
+
+  Inductive has_type : term -> type -> Prop :=
+  | T_True : has_type ttrue TBool
+  | T_False : has_type tfalse TBool
+  | T_If : forall t1 t2 t3 T,
+      has_type t1 TBool ->
+      has_type t2 T ->
+      has_type t3 T ->
+      has_type (iif t1 t2 t3) T
+  | T_Zero : has_type O TNat
+  | T_Succ : forall t1,
+      has_type t1 TNat ->
+      has_type (succ t1) TNat
+  | T_Pred : forall t1,
+      has_type t1 TNat ->
+      has_type (pred t1) TNat
+  | T_IsZero : forall t1,
+      has_type t1 TNat ->
+      has_type (iszero t1) TBool.
+
+  Lemma numeric_value_type : forall (t : term),
+    is_numeric_val t -> has_type t TNat.
+  Proof.
+    intros t H.
+    induction H as [| t' H' IH].
+    - apply T_Zero.
+    - apply T_Succ. exact IH.
+  Qed.
+
+  Inductive step : term -> term -> Prop :=
+  | E_IfTrue : forall t2 t3,
+      step (iif ttrue t2 t3) t2
+  | E_IfFalse : forall t2 t3,
+      step (iif tfalse t2 t3) t3
+  | E_If : forall t1 t1' t2 t3,
+      step t1 t1' ->
+      step (iif t1 t2 t3) (iif t1' t2 t3)
+  | E_Succ : forall t1 t1',
+      step t1 t1' ->
+      step (succ t1) (succ t1')
+  | E_PredZero :
+      step (pred O) O
+  | E_PredSucc : forall t1,
+      is_numeric_val t1 ->
+      step (pred (succ t1)) t1
+  | E_Pred : forall t1 t1',
+      step t1 t1' ->
+      step (pred t1) (pred t1')
+  | E_IsZeroZero :
+      step (iszero O) ttrue
+  | E_IsZeroSucc : forall t1,
+      is_numeric_val t1 ->
+      step (iszero (succ t1)) tfalse
+  | E_IsZero : forall t1 t1',
+      step t1 t1' ->
+      step (iszero t1) (iszero t1').
+
+  Lemma step_value_stuck : forall (t t' : term),
+    is_value t ->
+    step t t' ->
+    t = t'.
+  Proof.
+    intros t t' Hval Hstep.
+    destruct Hval.
+    - inversion Hstep.
+    - inversion Hstep.
+    - inversion Hstep. subst.
+      + inversion H.
+      +
+  Admitted.
+
+  (* 8.2.1 *)
+
+  Definition is_well_typed (t : term) : Prop :=
+    exists (T : type), has_type t T.
+
+  (* 8.2.2 *)
+  Lemma t_ttrue_inv : forall (T : type),
+    has_type ttrue T -> T = TBool.
+  Proof.
+    intros T H. inversion H. reflexivity.
+  Qed.
+
+  Lemma t_tfalse_inv : forall (T : type),
+    has_type tfalse T -> T = TBool.
+  Proof.
+    intros T H. inversion H. reflexivity.
+  Qed.
+
+  Lemma t_iff_inv : forall (t1 t2 t3 : term) (T : type),
+    has_type (iif t1 t2 t3) T ->
+    has_type t1 TBool /\ has_type t2 T /\ has_type t3 T.
+  Proof.
+    intros t1 t2 t3 T H.
+    inversion H as [| | | | | | H0 H1 H2].
+    split.
+    - exact H0.
+    - split.
+      + exact H1.
+      + exact H2.
+  Qed.
+
+  Lemma t_O_inv : forall T,
+    has_type O T -> T = TNat.
+  Proof.
+    intros T H. inversion H. reflexivity.
+  Qed.
+
+  Lemma t_succ_inv : forall (t1 : term) (T : type),
+    has_type (succ t1) T -> has_type t1 TNat /\ T = TNat.
+  Proof.
+    intros t1 T H.
+    inversion H as [| | | | | | H0 _].
+    split.
+    - exact H0.
+    - reflexivity.
+  Qed.
+
+  Lemma t_pred_inv : forall (t1 : term) (T : type),
+    has_type (pred t1) T -> has_type t1 TNat /\ T = TNat.
+  Proof.
+    intros t1 T H.
+    inversion H as [| | | | | | H0 _].
+    split.
+    - exact H0.
+    - reflexivity.
+  Qed.
+
+  Lemma t_iszero_inv : forall (t1 : term) (T : type),
+    has_type (iszero t1) T -> has_type t1 TNat /\ T = TBool.
+  Proof.
+    intros t1 T H.
+    inversion H as [| | | | | | H0 H1].
+    split.
+    - exact H1.
+    - reflexivity.
+  Qed.
+
+  (* 8.2.3 *)
+
+  Lemma wt_succ_inv : forall (t1 : term),
+    is_well_typed (succ t1) -> is_well_typed t1.
+  Proof.
+    intros t1 [T H].
+    apply t_succ_inv in H.
+    destruct H as [H1 _].
+    exists TNat.
+    exact H1.
+  Qed.
+
+  Lemma wt_pred_inv : forall (t1 : term),
+    is_well_typed (pred t1) -> is_well_typed t1.
+  Proof.
+    intros t1 [T H].
+    apply t_pred_inv in H.
+    destruct H as [H1 _].
+    exists TNat.
+    exact H1.
+  Qed.
+
+  Lemma wt_iszero_inv : forall (t1 : term),
+    is_well_typed (iszero t1) -> is_well_typed t1.
+  Proof.
+    intros t1 [T H].
+    apply t_iszero_inv in H.
+    destruct H as [H1 _].
+    exists TNat.
+    exact H1.
+  Qed.
+
+  Lemma wt_if_inv : forall (t1 t2 t3 : term),
+    is_well_typed (iif t1 t2 t3) -> is_well_typed t1 /\ is_well_typed t2 /\ is_well_typed t3.
+  Proof.
+    intros t1 t2 t3 [T H].
+    apply t_iff_inv in H.
+    destruct H as [H1 [H2 H3]].
+    split.
+    - exists TBool. exact H1.
+    - split.
+      + exists T. exact H2.
+      + exists T. exact H3.
+  Qed.
+
+  Inductive subterm : term -> term -> Prop :=
+  | subterm_refl : forall t, subterm t t
+  | subterm_if1 : forall t1 t2 t3 s,
+      subterm s t1 ->
+      subterm s (iif t1 t2 t3)
+  | subterm_if2 : forall t1 t2 t3 s,
+      subterm s t2 ->
+      subterm s (iif t1 t2 t3)
+  | subterm_if3 : forall t1 t2 t3 s,
+      subterm s t3 ->
+      subterm s (iif t1 t2 t3)
+  | subterm_succ : forall t1 s,
+      subterm s t1 ->
+      subterm s (succ t1)
+  | subterm_pred : forall t1 s,
+      subterm s t1 ->
+      subterm s (pred t1)
+  | subterm_iszero : forall t1 s,
+      subterm s t1 ->
+      subterm s (iszero t1).
+
+  Lemma subterms_typed : forall (t s : term) (T : type),
+    has_type t T ->
+    subterm s t ->
+    exists (T' : type), has_type s T'.
+  Proof.
+    intros t s T Htype Hst.
+    generalize dependent T.
+    induction Hst.
+    - intros T Htype. exists T. exact Htype.
+    - intros T Htype.
+      apply t_iff_inv in Htype.
+      destruct Htype as [H1 [_ _]].
+      apply IHHst in H1.
+      exact H1.
+    - intros T Htype.
+      apply t_iff_inv in Htype.
+      destruct Htype as [_ [H2 _]].
+      apply IHHst in H2.
+      exact H2.
+    - intros T Htype.
+      apply t_iff_inv in Htype.
+      destruct Htype as [_ [_ H3]].
+      apply IHHst in H3.
+      exact H3.
+    - intros T Htype.
+      apply t_succ_inv in Htype.
+      destruct Htype as [H1 _].
+      apply IHHst in H1.
+      exact H1.
+    - intros T Htype.
+      apply t_pred_inv in Htype.
+      destruct Htype as [H1 _].
+      apply IHHst in H1.
+      exact H1.
+    - intros T Htype.
+      apply t_iszero_inv in Htype.
+      destruct Htype as [H1 _].
+      apply IHHst in H1.
+      exact H1.
+  Qed.
+
+  (*
+    This is essentially the same as the previous lemma,
+    and it is piggybacking off it,
+    but it is stated with the is_well_typed predicate instead.
+  *)
+  Corollary subterms_welltyped : forall (t s : term),
+    is_well_typed t -> subterm s t -> is_well_typed s.
+  Proof.
+    intros t s Hwt Hst.
+    revert Hwt.
+    induction Hst.
+      - intros Hwt. exact Hwt.
+  Admitted.
+
+  (* 8.2.4 *)
+  Lemma uniqueness_of_types : forall (t : term) (T1 T2 : type),
+    has_type t T1 -> has_type t T2 -> T1 = T2.
+  Proof.
+    intros t T1 T2 H1 H2.
+    generalize dependent T2.
+    induction H1; intros T2 H2.
+    - apply t_ttrue_inv in H2. rewrite H2. reflexivity.
+    - apply t_tfalse_inv in H2. rewrite H2. reflexivity.
+    - apply t_iff_inv in H2.
+      destruct H2 as [_ [H2_2 _]].
+      apply IHhas_type2 in H2_2.
+      rewrite H2_2.
+      reflexivity.
+    - apply t_O_inv in H2. rewrite H2. reflexivity.
+    - apply t_succ_inv in H2.
+      destruct H2 as [_ H2_2].
+      rewrite H2_2.
+      reflexivity.
+    - apply t_pred_inv in H2.
+      destruct H2 as [_ H2_2].
+      rewrite H2_2.
+      reflexivity.
+    - apply t_iszero_inv in H2.
+      destruct H2 as [_ H2_2].
+      rewrite H2_2.
+      reflexivity.
+  Qed.
+
+  (* 8.3.1 *)
+  Lemma canonical_forms_bool : forall (t : term),
+    is_value t -> has_type t TBool -> t = ttrue \/ t = tfalse.
+  Proof.
+    intros t Hval Htype.
+    destruct Hval.
+    - left. reflexivity.
+    - right. reflexivity.
+    - apply numeric_value_type in H.
+      apply uniqueness_of_types with (T1 := TNat) in Htype; try assumption.
+      discriminate Htype.
+  Qed.
+
+  Lemma canonical_forms_nat : forall (t : term),
+    is_value t -> has_type t TNat -> is_numeric_val t.
+  Proof.
+    intros t Hval Htype.
+    destruct Hval.
+    - inversion Htype.
+    - inversion Htype.
+    - exact H.
+  Qed.
+
+  (* 8.3.2 *)
+  Lemma progress : forall (t : term) (T : type),
+    has_type t T -> is_value t \/ exists (t' : term), step t t'.
+  Proof.
+    intros t T Htype.
+    induction Htype.
+    (* T-True *)
+    - left. constructor.
+    (* T-False *)
+    - left. constructor.
+    (* T-If *)
+    - right. destruct IHHtype1 as [Hval1 | [t1' Hstep1]]; try assumption.
+      + apply canonical_forms_bool in Hval1; try assumption.
+        destruct Hval1 as [Htrue | Hfalse].
+        * exists t2. rewrite Htrue. constructor.
+        * exists t3. rewrite Hfalse. constructor.
+      + exists (iif t1' t2 t3). constructor. exact Hstep1.
+    (* T-Zero *)
+    - left. constructor. constructor.
+    (* T-Succ *)
+    - destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
+      + apply canonical_forms_nat in Hval1; try assumption.
+        left.
+        apply nv_succ in Hval1.
+        apply numeric_value_is_value in Hval1.
+        exact Hval1.
+      + right.
+        exists (succ t1').
+        constructor.
+        exact Hstep1.
+    (* T-Pred *)
+    - destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
+      + apply canonical_forms_nat in Hval1; try assumption.
+        right.
+        destruct Hval1 as [| t1'' Hnv].
+        * exists O. constructor.
+        * exists t1''. constructor. exact Hnv.
+      + right.
+        exists (pred t1').
+        constructor.
+        exact Hstep1.
+    (* T-IsZero *)
+    - destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
+      + apply canonical_forms_nat in Hval1; try assumption.
+        right.
+        destruct Hval1 as [| t1'' Hnv].
+        * exists ttrue. constructor.
+        * exists tfalse. constructor. exact Hnv.
+      + right.
+        exists (iszero t1').
+        constructor.
+        exact Hstep1.
+  Qed.
+
+  (* 8.3.3 *)
+  Lemma preservation : forall (t t' : term) (T : type),
+    has_type t T -> step t t' -> has_type t' T.
+  Proof.
+    intros t t' T Htype Hstep.
+    generalize dependent t'.
+    (* Induction on the typing derivation *)
+    induction Htype; intros t' Hstep.
+    (* T-True *)
+    - inversion Hstep.
+    (* T-False *)
+    - inversion Hstep.
+    (* T-If *)
+    - inversion Hstep; subst.
+      + (* E-IfTrue *)
+        assumption.
+      + (* E-IfFalse *)
+        assumption.
+      + (* E-If *)
+        apply T_If; try assumption. apply IHHtype1. assumption.
+    (* T-Zero *)
+    - inversion Hstep.
+    (* T-Succ *)
+    - inversion Hstep; subst.
+      + (* E-Succ *)
+        apply T_Succ. apply IHHtype. assumption.
+    (* T-Pred *)
+    - inversion Hstep; subst.
+      + (* E-PredZero *)
+        apply T_Zero.
+      + (* E-PredSucc *)
+        apply numeric_value_type. assumption.
+      + (* E-Pred *)
+        apply T_Pred. apply IHHtype. assumption.
+    (* T-IsZero *)
+    - inversion Hstep; subst.
+      + (* E-IsZeroZero *)
+        apply T_True.
+      + (* E-IsZeroSucc *)
+        apply T_False.
+      + (* E-IsZero *)
+        apply T_IsZero. apply IHHtype. assumption.
+  Qed.
+
+  (* 8.3.3 *)
+  Lemma preservation_by_eval_drvs : forall (t t' : term) (T : type),
+    has_type t T -> step t t' -> has_type t' T.
+  Proof.
+    intros t t' T Htype Hstep.
+    generalize dependent T.
+    (* Induction on the evaluation derivation *)
+    induction Hstep; intros T Htype.
+    (* E-IfTrue *)
+    - apply t_iff_inv in Htype.
+      destruct Htype as [H1 [H2 H3]].
+      assumption.
+    (* E-IfFalse *)
+    - apply t_iff_inv in Htype.
+      destruct Htype as [H1 [H2 H3]].
+      assumption.
+    (* E-If *)
+    - apply t_iff_inv in Htype.
+      destruct Htype as [H1 [H2 H3]].
+      apply T_If; try assumption.
+      apply IHHstep. exact H1.
+    (* E-Succ *)
+    - apply t_succ_inv in Htype.
+      destruct Htype as [H1 H2].
+      apply IHHstep in H1.
+      rewrite H2.
+      apply T_Succ.
+      exact H1.
+    (* E-PredZero *)
+    - apply t_pred_inv in Htype.
+      destruct Htype as [H1 H2].
+      rewrite H2.
+      apply T_Zero.
+    (* E-PredSucc *)
+    - apply t_pred_inv in Htype.
+      destruct Htype as [H1 H2].
+      rewrite H2.
+      apply numeric_value_type.
+      exact H.
+    (* E-Pred *)
+    - apply t_pred_inv in Htype.
+      destruct Htype as [H1 H2].
+      apply IHHstep in H1.
+      rewrite H2.
+      apply T_Pred.
+      exact H1.
+    (* E-IsZeroZero *)
+    - apply t_iszero_inv in Htype.
+      destruct Htype as [H1 H2].
+      rewrite H2.
+      apply T_True.
+    (* E-IsZeroSucc *)
+    - apply t_iszero_inv in Htype.
+      destruct Htype as [H1 H2].
+      rewrite H2.
+      apply T_False.
+    (* E-IsZero *)
+    - apply t_iszero_inv in Htype.
+      destruct Htype as [H1 H2].
+      apply IHHstep in H1.
+      rewrite H2.
+      apply T_IsZero.
+      exact H1.
+  Qed.
+
+  (* 8.3.6 *)
+  Lemma not_subject_expansion : ~(
+    forall (t t' : term) (T : type),
+    step t t' ->
+    has_type t' T ->
+    has_type t T
+  ).
+  Proof.
+    intros H.
+    specialize (H (iif ttrue O ttrue) O TNat).
+    assert (has_type (iif ttrue O ttrue) TNat).
+    { apply H.
+      - constructor.
+      - constructor.
+    }
+    inversion H0 as [| | | | | | H1 H2 H3].
+    inversion H3.
+  Qed.
+
+  (* 8.3.7 *)
+  Inductive step_big : term -> term -> Prop :=
+  | B_Value : forall (t : term),
+    is_value t ->
+    step_big t t
+  | B_IfTrue : forall (t1 t2 t3 v2 : term),
+    step_big t1 ttrue ->
+    is_value v2 ->
+    step_big t2 v2 ->
+    step_big (iif ttrue t2 t3) v2
+  | B_IfFalse : forall (t1 t2 t3 v3 : term),
+    step_big t1 tfalse ->
+    is_value v3 ->
+    step_big t3 v3 ->
+    step_big (iif tfalse t2 t3) v3
+  | B_Succ : forall (t1 nv1 : term),
+    is_numeric_val nv1 ->
+    step_big t1 nv1 ->
+    step_big (succ t1) (succ nv1)
+  | B_PredZero : forall (t1 : term),
+    step_big t1 O ->
+    step_big (pred O) O
+  | B_PredSucc : forall (t1 nv1 : term),
+    is_numeric_val nv1 ->
+    step_big t1 (succ nv1) ->
+    step_big (pred t1) nv1
+  | B_IsZeroZero : forall (t1 : term),
+    step_big t1 O ->
+    step_big (iszero t1) ttrue
+  | B_IsZeroSucc : forall (t1 nv1 : term),
+    is_numeric_val nv1 ->
+    step_big t1 (succ nv1) ->
+    step_big (iszero t1) tfalse.
+
+  Lemma big_step_progress : forall (t : term) (T : type),
+    has_type t T -> is_value t \/ exists (t' : term), step_big t t'.
+  Proof.
+    intros t T Htype.
+    induction Htype.
+    (* T-True *)
+    - left. constructor.
+    (* T-False *)
+    - left. constructor.
+    (* T-If *)
+    - destruct IHHtype1 as [Hval1 | [t1' Hstep1]]; try assumption.
+      + right. apply canonical_forms_bool in Hval1; try assumption.
+        destruct Hval1 as [Htrue | Hfalse].
+        * exists t2. rewrite Htrue.
+  Admitted.
+
+  Lemma big_step_preservation : forall (t t' : term) (T : type),
+    has_type t T -> step_big t t' -> has_type t' T.
+  Proof.
+    intros t t' T Htype Hstep.
+    generalize dependent t'.
+    induction Htype; intros t' Hstep.
+    (* T-True *)
+    - inversion Hstep; subst. apply T_True.
+    (* T-False *)
+    - inversion Hstep; subst. apply T_False.
+    (* T-If *)
+    - inversion Hstep; subst.
+      + apply T_If; try assumption.
+      + apply IHHtype2. assumption.
+      + apply IHHtype3. assumption.
+    (* T-Zero *)
+    - inversion Hstep; subst. apply T_Zero.
+    (* T-Succ *)
+    - inversion Hstep; subst.
+      + apply T_Succ. exact Htype.
+      + apply T_Succ. apply IHHtype. assumption.
+    (* T-Pred *)
+    - inversion Hstep; subst.
+      + apply T_Pred. assumption.
+      + assumption.
+      + apply IHHtype in H1.
+        apply t_succ_inv in H1.
+        apply H1.
+    (* T-IsZero *)
+    - inversion Hstep; subst.
+      + apply T_IsZero. assumption.
+      + apply T_True.
+      + apply T_False.
+  Qed.
+
+  (* 8.3.8 *)
+  (* Inductive term2 : Type :=
+  | ttrue
+  | tfalse
+  | iif (t1 t2 t3 : term2)
+  | O
+  | succ (t : term2)
+  | pred (t : term2)
+  | iszero (t : term2)
+  | wrong. *)
+End Chap8.
\ No newline at end of file