diff --git a/advanced.ipynb b/advanced.ipynb
index 427028d..7713a55 100644
--- a/advanced.ipynb
+++ b/advanced.ipynb
@@ -1,1293 +1,1288 @@
 {
  "cells": [
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "Adapted from a workshop given at [POPL\n",
     "2008](https://www.cis.upenn.edu/~plclub/popl08-tutorial/).\n",
     "\n",
     "The NB language, back again\n",
     "===========================\n",
     "\n",
     "In this notebook, we will be working with a language very similar to the\n",
     "NB language from the first assignment.\n",
     "\n",
     "Definitions\n",
     "-----------\n",
     "\n",
     "### Grammar and terms\n",
     "\n",
     "The grammar of our language would be defined as follows:\n",
     "\n",
     "    t  ::= \"true\"                   terms\n",
     "         | \"false\"\n",
     "         | \"if\" t \"then\" t \"else\" t\n",
     "         | 0\n",
     "         | \"succ\" t\n",
     "         | \"pred\" t\n",
     "         | \"iszero\" t\n",
     "\n",
     "To represent the terms of this language in Coq, we will define `tm`, an\n",
     "`Inductive` data type:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Inductive tm : Set :=\n",
     "| tm_true : tm\n",
     "| tm_false : tm\n",
     "| tm_if : tm -> tm -> tm -> tm\n",
     "| tm_zero : tm\n",
     "| tm_succ : tm -> tm\n",
     "| tm_pred : tm -> tm\n",
     "| tm_iszero : tm -> tm."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "Compare the two definitions. For every rule in the grammar, there is a\n",
     "corresponding *constructor*. Each constructor is a value in Coq that\n",
     "allows us to obtain values of type `tm`. In contrast to the previous\n",
     "notebook, here we annotate every constructor with a type. `tm_true` is a\n",
     "constructor corresponding to the terminal rule `\"true\"` - it takes no\n",
     "arguments and is therefore annotated with the simple type `tm`.\n",
     "`tm_succ` is a constructor corresponding to the `\"succ\" t` rule - since\n",
     "the rule has a single subterm, the constructor is a function from `tm`\n",
     "to `tm`.\n",
     "\n",
     "Using the above definition, we can create values corresponding to the\n",
     "terms in our language:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "(* Represents \"if (iszero 0) false true\" *)\n",
     "Check (tm_if (tm_iszero tm_zero) tm_false tm_true)."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "### Definition of value\n",
     "\n",
     "Next, we want to define what it means to be a *value* in our language.\n",
     "While in the original NB language we did so through grammar rules, it’s\n",
     "equally valid to define a judgment which tells us which terms are\n",
     "boolean and numeric values (correspondingly, `bvalue` and `nvalue`):\n",
     "\n",
     "      ---------------  (b_true)\n",
     "      ⊢ bvalue (true)\n",
     "\n",
     "      ---------------- (b_false)\n",
     "      ⊢ bvalue (false)\n",
     "\n",
     "      \n",
     "      ---------- (n_zero)\n",
     "      ⊢ nvalue 0\n",
     "      \n",
     "         ⊢ nvalue t\n",
     "      ----------------- (n_succ)\n",
     "      ⊢ nvalue (succ t)\n",
     "\n",
     "Recall that from Curry-Howard correspondence we know that types\n",
     "correspond to propositions and values correspond to proofs. Therefore,\n",
     "we can represent the above judgements in Coq by defining types\n",
     "corresponding to the judgments. Those types are `bvalue t` and\n",
     "`nvalue t`. Being able to create a well-typed value of type `nvalue t`\n",
     "is the same as being able to construct a proof that a given term is an\n",
     "`nvalue`; same notion applies to `bvalue t`.\n",
     "\n",
     "We define said types as follows:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Inductive bvalue : tm -> Prop := \n",
     "| b_true : bvalue tm_true \n",
     "| b_false : bvalue tm_false.\n",
     "\n",
     "Inductive nvalue : tm -> Prop :=\n",
     "| n_zero : nvalue tm_zero\n",
     "| n_succ : forall t,\n",
     "    nvalue t ->\n",
     "    nvalue (tm_succ t)."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "Those definitions should look similar to the inference rules above,\n",
     "although they may also look slightly confusing. Before trying to\n",
     "understand their every part, it may help to see how they are meant to be\n",
     "used.\n",
     "\n",
     "Again, the *type* `nvalue t` represents the *proposition* that `t` is a\n",
     "numeric value. For instance, `nvalue (tm_succ tm_zero)` represents the\n",
     "proposition that the successor of zero (or simply one) is a numeric\n",
     "value. To show that this proposition is true, we need to construct a\n",
     "value of said type. We can do that as follows:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Check (n_succ tm_zero n_zero)."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "You should now go back to the definitions and try to understand how they\n",
     "represent their corresponding inference rules.\n",
     "\n",
     "One thing that may still be puzzling are the `Set` and `tm -> Prop`\n",
     "annotation. If you are suspecting that the second one mentions `tm ->`\n",
     "because the corresponding type is a *type-level function* from `tm` to\n",
     "`Prop`, you’d be correct:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Check nvalue.\n",
     "Check nvalue tm_zero."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "The difference between `Set` and `Prop` is much more subtle and\n",
     "fundamental. To put it briefly, types annotated as `Set` are meant to be\n",
     "used as data types, while those annotated as `Prop` are meant to be used\n",
     "as propositions. Fully explaining this distinction is beyond the scope\n",
     "of this course, but the above intuition should serve you well enough.\n",
     "\n",
     "As the last thing in this section, we will (finally) define what it\n",
     "means to be a value. If you recall that `T \\/ S` is the data type\n",
     "corresponding to the proof that either `T` or `S`, the definition is\n",
     "simple enough:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
-    "Inductive value : t -> Prop :=\n",
-    "| v_bvalue : forall t,\n",
-    "    bvalue t ->\n",
-    "    value t\n",
-    "| v_nvalue : forall t,\n",
-    "    nvalue t ->\n",
-    "    value t"
+    "Definition value (t : tm) : Prop :=\n",
+    "  bvalue t \\/ nvalue t."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "### Operational semantics\n",
     "\n",
     "Having defined `tm`s and `value`s, we can define call-by-value\n",
     "operational semantics for our language. We will define an inductive data\n",
     "type `eval (t : tm) (t' : tm) : Prop` corresponding to the proposition\n",
     "that `t` evaluates to `t'` in a single step. The definition is as\n",
     "follows:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Inductive eval : tm -> tm -> Prop :=\n",
     "| e_iftrue : forall t2 t3,\n",
     "    eval (tm_if tm_true t2 t3) t2\n",
     "| e_iffalse : forall t2 t3,\n",
     "    eval (tm_if tm_false t2 t3) t3\n",
     "| e_if : forall t1 t1' t2 t3,\n",
     "    eval t1 t1' ->\n",
     "    eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)\n",
     "| e_succ : forall t t',\n",
     "    eval t t' ->\n",
     "    eval (tm_succ t) (tm_succ t')\n",
     "| e_predzero :\n",
     "    eval (tm_pred tm_zero) tm_zero\n",
     "| e_predsucc : forall t,\n",
     "    nvalue t ->\n",
     "    eval (tm_pred (tm_succ t)) t\n",
     "| e_pred : forall t t',\n",
     "    eval t t' ->\n",
     "    eval (tm_pred t) (tm_pred t')\n",
     "| e_iszerozero :\n",
     "    eval (tm_iszero tm_zero) tm_true\n",
     "| e_iszerosucc : forall t,\n",
     "    nvalue t ->\n",
     "    eval (tm_iszero (tm_succ t)) tm_false\n",
     "| e_iszero : forall t t',\n",
     "    eval t t' ->\n",
     "    eval (tm_iszero t) (tm_iszero t')."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "If you don’t feel comfortable with Coq syntax yet, compare the above\n",
     "with the definition of beta-reduction from our first assignment.\n",
     "\n",
     "Next, we define the multi-step evaluation relation `eval_many`,\n",
     "corresponding to multi-step beta-reduction.\n",
     "\n",
     "Its inference rules are:\n",
     "\n",
     "     -------------  (m_refl)\n",
     "     eval_many t t \n",
     "     \n",
     "     eval t t'    eval_many t' u\n",
     "     ---------------------------  (m_step)\n",
     "           eval_many t u\n",
     "\n",
     "And its definition is:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Inductive eval_many : tm -> tm -> Prop :=\n",
     "| m_refl : forall t,\n",
     "    eval_many t t\n",
     "| m_step : forall t t' u,\n",
     "    eval t t' ->\n",
     "    eval_many t' u ->\n",
     "    eval_many t u."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "### Exercises\n",
     "\n",
     "**Note** The exercises below may be hard. If you find yourself stuck\n",
     "when doing them, copy the definitions from solutions here - they will be\n",
     "useful later on.\n",
     "\n",
     "**Exercise** Multi-step evaluation is often defined as the “reflexive,\n",
     "transitive closure” of single-step evaluation. Write an inductively\n",
     "defined relation `eval_rtc` that corresponds to that verbal description.\n",
     "\n",
     "In case you get stuck or need a hint, you can find solutions to all the\n",
     "exercises near the bottom of the file.\n",
     "\n",
     "**Exercise** Sometimes it is more convenient to use a big-step semantics\n",
     "for a language. Add the remaining constructors to finish the inductive\n",
     "definition `full_eval` for the big-step semantics that corresponds to\n",
     "the small-step semantics defined by `eval`. Build the inference rules so\n",
     "that `full_eval t v` logically implies both `eval_many t v` and\n",
     "`value v`. In order to do this, you may need to add the premise\n",
     "`nvalue v` to the appropriate cases.\n",
     "\n",
     "Hint: You should end up with a total of 8 cases.\n",
     "\n",
     "    Inductive full_eval : tm -> tm -> Prop :=\n",
     "    | f_value : forall v,\n",
     "        value v ->\n",
     "        full_eval v v\n",
     "    | f_iftrue : forall t1 t2 t3 v,\n",
     "        full_eval t1 tm_true ->\n",
     "        full_eval t2 v ->\n",
     "        full_eval (tm_if t1 t2 t3) v\n",
     "    | f_succ : forall t v,\n",
     "        nvalue v ->\n",
     "        full_eval t v ->\n",
     "        full_eval (tm_succ t) (tm_succ v).\n",
     "\n",
     "Proofs\n",
     "------\n",
     "\n",
     "So far, we’ve only seen proofs represented in Coq as\n",
     "manually-constructed values. For any non-trivial proof value, it’s\n",
     "rather inconvenient to manually construct it.\n",
     "\n",
     "Proof values are most easily built interactively, using tactics to\n",
     "manipulate a proof state. A proof state consists of a set of goals\n",
     "(propositions or types for which you must produce an inhabitant), each\n",
     "with a context of hypotheses (inhabitants of propositions or types you\n",
     "are allowed to use). A proof state begins initially with one goal (the\n",
     "statement of the lemma you are trying to prove) and no hypotheses. A\n",
     "goal can be solved, and thereby eliminated, when it exactly matches one\n",
     "of hypotheses in the context. A proof is completed when all goals are\n",
     "solved.\n",
     "\n",
     "Tactics can be used for forward reasoning (which, roughly speaking,\n",
     "means modifying the hypotheses of a context while leaving the goal\n",
     "unchanged) or backward reasoning (replacing the current goal with one or\n",
     "more new goals in simpler contexts). Given the level of detail required\n",
     "in a formal proof, it would be ridiculously impractical to complete a\n",
     "proof using forward reasoning alone. However it is usually both possible\n",
     "and practical to complete a proof using backward reasoning alone.\n",
     "Therefore, we focus almost exclusively on backward reasoning in this\n",
     "tutorial. Of course, most people naturally use a significant amount of\n",
     "forward reasoning in their thinking process, so it may take you a while\n",
     "to become accustomed to getting by without it.\n",
     "\n",
     "We use the keyword `Lemma` to state a new proposition we wish to prove.\n",
     "(`Theorem` and `Fact` are exact synonyms for `Lemma`.) The keyword\n",
     "`Proof`, immediately following the statement of the proposition,\n",
     "indicates the beginning of a proof script. A proof script is a sequence\n",
     "of tactic expressions, each concluding with a `.`. Once all of the goals\n",
     "are solved, we use the keyword `Qed` to record the completed proof. If\n",
     "the proof is incomplete, we may tell Coq to accept the lemma on faith by\n",
     "using `Admitted` instead of `Qed`.\n",
     "\n",
     "We now proceed to introduce the specific proof tactics.\n",
     "\n",
     "### Implication and universal quantification\n",
     "\n",
     "        - [intros]\n",
     "        - [apply]\n",
     "        - [apply with (x := ...)]\n",
     "\n",
     "Recall that both implication and universal quantification correspond to\n",
     "function types and values. Accordingly, we can use the `intros` tactic\n",
     "to move universally quantified variables and implication antecedents\n",
     "from the goal into the context as hypotheses.\n",
     "\n",
     "If our current goal corresponds to a conclusion of some implication `P`,\n",
     "we can use the `apply P` tactic to prove our goal by proving the\n",
     "antecedents of `P`. If you’d suspect from the name of the tactic that\n",
     "this corresponds to applying a function, you’d be correct. Using `apply`\n",
     "allows building a proof value from the bottom up.\n",
     "\n",
     "#### Example 1\n",
     "\n",
     "In the following example, we will create a value corresponding to a\n",
     "(still) simple proposition. Step through every cell below to see how\n",
     "this value is constructed."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma e_succ_pred_succ : forall t,\n",
     "  nvalue t ->\n",
     "  eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t).\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** Let [t] be a [tm]. *)\n",
     "  intros t."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** Assume that [t] is an [nvalue] (and let's call that\n",
     "      assumption [Hn] for future reference). *)\n",
     "  intros Hn."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** By [e_succ], in order to prove our conclusion, it suffices\n",
     "      to prove that [eval (tm_pred (tm_succ t)) t]. *)\n",
     "  Check e_succ.\n",
     "  apply e_succ."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** That, in turn, can be shown by [e_predsucc], if we are\n",
     "      able to show that [nvalue t]. *)\n",
     "  Check e_predsucc.\n",
     "  apply e_predsucc."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** But, in fact, we assumed [nvalue t]. *)\n",
     "  apply Hn."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "At this point, we have successfully concluded our proof;\n",
     "`e_succ_pred_succ` is a value that can be used like any other value we\n",
     "have seen so far. It corresponds to the following proof tree:\n",
     "\n",
     "                            nvalue t\n",
     "                 ---------------------------- (e_predsucc)\n",
     "                 eval (tm_pred (tm_succ t)) t\n",
     "        ------------------------------------------------ (e_succ)\n",
     "        eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)\n",
     "\n",
     "We can see the value we have constructed with the following command:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Print e_succ_pred_succ."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "Compare the value to the proof script above. Observe how function\n",
     "application in the value corresponds to usages of `apply` tactic.\n",
     "\n",
     "#### Example 2\n",
     "\n",
     "Now consider, for a moment, the rule `m_step`:\n",
     "\n",
     "        eval t t'  eval_many t' u\n",
     "        ------------------------- (m_step)\n",
     "              eval_many t u\n",
     "\n",
     "If we have a goal such as `eval_many e1 e2`, we should be able to use\n",
     "`apply m_step` in order to replace it with the goals `eval e1 t'` and\n",
     "`eval_many t' e2`. But what exactly is `t'` here? When and how is it\n",
     "chosen? It stands to reason the conclusion is justified if we can come\n",
     "up with any `t'` for which the premises can be justified.\n",
     "\n",
     "Now we note that, in the Coq syntax for the type of `m_step`, all three\n",
     "variables `t`, `t'`, and `u` are universally quantified. The tactic\n",
     "`apply m_step` will use pattern matching between our goal and the\n",
     "conclusion of `m_step` to find the only possible instantiation of `t`\n",
     "and `u`. However, `apply m_step` will raise an error since it does not\n",
     "know how it should instantiate `t'`. In this case, the `apply` tactic\n",
     "takes a `with` clause that allows us to provide this instantiation. This\n",
     "is demonstrated in the proof below.\n",
     "\n",
     "Observe how this works in the proof script below. The proof tree here\n",
     "gives a visual representation of the proof term we are going to\n",
     "construct and the proof script has again been annotated with the steps\n",
     "in English.\n",
     "\n",
     "        Letting   s = tm_succ\n",
     "                  p = tm_pred\n",
     "                lem = e_succ_pred_succ,\n",
     "\n",
     "                nvalue t\n",
     "        - - - - - - - - - - - - (lem)    --------------------- (m_refl)\n",
     "        eval (s (p (s t))) (s t)         eval_many (s t) (s t)\n",
     "        ------------------------------------------------------ (m_step)\n",
     "                      eval_many (s (p (s t))) (s t)"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_succ_pred_succ : forall t,\n",
     "  nvalue t ->\n",
     "  eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** Let [t] be a [tm], and assume [nvalue t]. *)\n",
     "  intros t Hn."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** By [m_step], to show our conclusion, it suffices to find\n",
     "      some [t'] for which\n",
     "        [eval (tm_succ (tm_pred (tm_succ t))) t']\n",
     "      and\n",
     "        [eval t' (tm_succ t)].\n",
     "      Let us choose [t'] to be [tm_succ t]. *)\n",
     "  Check m_step.\n",
     "  apply m_step with (t' := tm_succ t)."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "    (** By the lemma [e_succ_pred_succ], to show\n",
     "          [eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)],\n",
     "        it suffices to show [nvalue t]. *)\n",
     "    Check e_succ_pred_succ.\n",
     "    apply e_succ_pred_succ."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "    (** And, in fact, we assumed [nvalue t]. *)\n",
     "    apply Hn."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "    (** Moreover, by the rule [m_refl], we also may conclude\n",
     "        [eval (tm_succ t) (tm_succ t)]. *)\n",
     "    Check m_refl.\n",
     "    apply m_refl."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "#### Lab 1\n",
     "\n",
     "Write proof scripts for the following lemmas, following the plain\n",
     "language descriptions.\n",
     "\n",
     "These lemmas will be useful in later proofs."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_one : forall t1 t2,\n",
     "  eval t1 t2 ->\n",
     "  eval_many t1 t2."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** Let [t1] and [t2] be terms, and assume [eval t1 t2].  We\n",
     "      may conclude [eval_many t1 t2] by [m_step] if we can find\n",
     "      a term [t'] such that [eval t1 t'] and [eval_many t' t2].\n",
     "      We will choose [t'] to be [t2].  Now we can show\n",
     "      [eval t1 t2] by our assumption, and we can show\n",
     "      [eval_many t2 t2] by [m_refl]. *)\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* to finish *)\n",
     "Admitted."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_two : forall t1 t2 t3,\n",
     "  eval t1 t2 ->\n",
     "  eval t2 t3 ->\n",
     "  eval_many t1 t3."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** Let [t1], [t2], and [t3] be terms.  Assume [eval t1 t2]\n",
     "      and [eval t2 t3].  By [m_step], we may conclude that\n",
     "      [eval_many t1 t3] if we can find a term [t'] such that\n",
     "      [eval t1 t'] and [eval_many t' t3].  Let's choose [t'] to\n",
     "      be [t2].  We know [eval t1 t2] holds by assumption.  In\n",
     "      the other case, by the lemma [m_one], to show [eval_many\n",
     "      t2 t3], it suffices to show [eval t2 t3], which is one of\n",
     "      our assumptions.  *)\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* to finish *)\n",
     "Admitted."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_iftrue_step : forall t t1 t2 u,\n",
     "  eval t tm_true ->\n",
     "  eval_many t1 u ->\n",
     "  eval_many (tm_if t t1 t2) u."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** Let [t], [t1], [t2], and [u] be terms.  Assume that\n",
     "      [eval t tm_true] and [eval_many t1 u].  To show\n",
     "      [eval_many (tm_if t t1 t2) u], by [m_step], it suffices to\n",
     "      find a [t'] for which [eval (tm_if t t1 t2) t'] and\n",
     "      [eval_many t' u].  Let us choose [t'] to be\n",
     "      [tm_if tm_true t1 t2].  Now we can use [e_if] to show that\n",
     "      [eval (tm_if t t1 t2) (tm_if tm_true t1 t2)] if we can\n",
     "      show [eval t tm_true], which is actually one of our\n",
     "      assumptions.  Moreover, using [m_step] once more, we can\n",
     "      show [eval_many (tm_if tm_true t1 t2) u] where [t'] is\n",
     "      chosen to be [t1].  Doing so leaves us to show\n",
     "      [eval (tm_if tm_true t1 t2) t1] and [eval_many t1 u].  The\n",
     "      former holds by [e_iftrue] and the latter holds by\n",
     "      assumption. *)\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* to finish *)\n",
     "Admitted."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "### Working with Conjunction and Disjunction\n",
     "\n",
     "        - [split]\n",
     "        - [left]\n",
     "        - [right]\n",
     "        - [destruct] (for conjunction and disjunction)\n",
     "\n",
     "**Example** If `H` is the name of a conjunctive hypothesis, then\n",
     "`destruct H as p` will replace the hypothesis `H` with its components\n",
     "using the names in the pattern `p`. Observe the pattern in the example\n",
     "below."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_two_conj : forall t t' t'',\n",
     "  eval t t' /\\ eval t' t'' ->\n",
     "  eval_many t t''.\n",
     "Proof.\n",
     "  intros t t' t'' H.\n",
     "   destruct H as [ He1 He2 ].\n",
     "   apply m_two with (t2 := t').\n",
     "    apply He1.\n",
     "    apply He2.\n",
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "**Example** Patterns may be nested to break apart nested structures.\n",
     "Note that infix conjunction is right-associative, which is significant\n",
     "when trying to write nested patterns. We will later see how to use\n",
     "`destruct` on many different sorts of hypotheses."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_three_conj : forall t t' t'' t''',\n",
     "  eval t t' /\\ eval t' t'' /\\ eval t'' t''' ->\n",
     "  eval_many t t'''.\n",
     "Proof.\n",
     "  intros t t' t'' t''' H.\n",
     "   destruct H as [ He1 [ He2 He3 ] ].\n",
     "   apply m_step with (t' := t').\n",
     "    apply He1.\n",
     "    apply m_two with (t2 := t'').\n",
     "      apply He2.\n",
     "      apply He3.\n",
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "**Example** If your goal is a conjunction, use `split` to break it apart\n",
     "into two separate subgoals."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_three : forall t t' t'' t''',\n",
     "  eval t t' ->\n",
     "  eval t' t'' ->\n",
     "  eval t'' t''' ->\n",
     "  eval_many t t'''.\n",
     "Proof.\n",
     "  intros t t' t'' t''' He1 He2 He3.\n",
     "   apply m_three_conj with (t' := t') (t'' := t'').\n",
     "    split.\n",
     "      apply He1.\n",
     "      split.\n",
     "        apply He2.\n",
     "        apply He3.\n",
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "**Exercise** Hint: You might find lemma `m_three` useful here."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_if_iszero_conj : forall v t2 t2' t3 t3',\n",
     "  nvalue v /\\ eval t2 t2' /\\ eval t3 t3' ->\n",
     "  eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\\\n",
     "  eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* to finish *)\n",
     "Admitted."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "**Example** If we have a disjunction in the context, we can use\n",
     "`destruct` to reason by cases on the hypothesis. Note the syntax of the\n",
     "associated pattern."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma e_if_true_or_false : forall t1 t2,\n",
     "  eval t1 tm_true \\/ eval t1 tm_false ->\n",
     "  eval_many (tm_if t1 t2 t2) t2.\n",
     "Proof.\n",
     "  intros t1 t2 H. destruct H as [ He1 | He2 ].\n",
     "    apply m_two with (t2 := tm_if tm_true t2 t2).\n",
     "      apply e_if. apply He1.\n",
     "      apply e_iftrue.\n",
     "    apply m_two with (t2 := tm_if tm_false t2 t2).\n",
     "      apply e_if. apply He2.\n",
     "      apply e_iffalse.\n",
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "Reasoning by Cases and Induction\n",
     "--------------------------------\n",
     "\n",
     "        - [destruct] (for inductively defined propositions)\n",
     "        - [induction]\n",
     "\n",
     "**Example** Use `destruct` to reason by cases on an inductively defined\n",
     "datatype or proposition."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma e_iszero_nvalue : forall v,\n",
     "  nvalue v ->\n",
     "  eval (tm_iszero v) tm_true \\/\n",
     "  eval (tm_iszero v) tm_false.\n",
     "Proof.\n",
     "  intros v Hn."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  destruct Hn."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* Case [n_zero].\n",
     "     Note how [v] becomes [tm_zero] in the goal. *)\n",
     "    left."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "    apply e_iszerozero."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* Case [n_succ].\n",
     "     Note how [v] becomes [tm_succ v] in the goal. *)\n",
     "    right."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "    apply e_iszerosucc. apply Hn.\n",
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "**Example** You can use `induction` to reason by induction on an\n",
     "inductively defined datatype or proposition. This is the same as\n",
     "`destruct`, except that it also introduces an induction hypothesis in\n",
     "the inductive cases."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_iszero : forall t u,\n",
     "  eval_many t u ->\n",
     "  eval_many (tm_iszero t) (tm_iszero u).\n",
     "Proof.\n",
     "  intros t u Hm. induction Hm.\n",
     "    apply m_refl.\n",
     "    apply m_step with (t' := tm_iszero t').\n",
     "      apply e_iszero. apply H.\n",
     "      apply IHHm.\n",
     "Qed."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "#### Lab 3\n",
     "\n",
     "Work on the following exercise.\n",
     "\n",
     "**Exercise**"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Lemma m_trans : forall t t' u,\n",
     "  eval_many t t' ->\n",
     "  eval_many t' u ->\n",
     "  eval_many t u."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (** We proceed by induction on the derivation of\n",
     "      [eval_many t t'].\n",
     "      Case [m_refl]: Since [t] and [t'] must be the same, our\n",
     "        conclusion holds by assumption.\n",
     "      Case [m_step]: Now let's rename the [t'] from the lemma\n",
     "        statement to [u0] (as Coq likely will) and observe that\n",
     "        there must be some [t'] (from above the line of the\n",
     "        [m_step] rule) such that [eval t t'] and\n",
     "        [eval_many t' u0].  Our conclusion follows from from\n",
     "        an application of [m_step] with our new [t'] and our\n",
     "        induction hypothesis, which allows us to piece together\n",
     "        [eval_many t' u0] and [eval_many u0 u] to get\n",
     "        [eval_many t' u]. *)\n",
     "Proof."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "  (* to finish *)\n",
     "Admitted."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
     "**Exercise** Prove the following lemma.\n",
     "\n",
     "Hint: You may be interested in some previously proved lemmas, such as\n",
     "`m_one` and `m_trans`.\n",
     "\n",
     "Note: Even though this lemma is in a comment, its solution is also at\n",
     "the bottom. (Coq will give an error if we leave it uncommented since it\n",
     "mentions the `eval_rtc` relation, which was the solution to another\n",
     "exercise.)\n",
     "\n",
     "    Lemma eval_rtc_many : forall t u,\n",
     "      eval_rtc t u ->\n",
     "      eval_many t u.\n",
     "\n",
     "**Exercise** Prove the following lemma.\n",
     "\n",
     "    Lemma eval_many_rtc : forall t u,\n",
     "      eval_many t u ->\n",
     "      eval_rtc t u.\n",
     "\n",
     "**Exercise** Prove the following lemma.\n",
     "\n",
     "    Lemma full_eval_to_value : forall t v,\n",
     "      full_eval t v ->\n",
     "      value v.\n",
     "\n",
     "Solutions to Exercises\n",
     "======================"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "Inductive eval_rtc : tm -> tm -> Prop :=\n",
     "| r_eval : forall t t',\n",
     "    eval t t' ->\n",
     "    eval_rtc t t'\n",
     "| r_refl : forall t,\n",
     "    eval_rtc t t\n",
     "| r_trans : forall t u v,\n",
     "    eval_rtc t u ->\n",
     "    eval_rtc u v ->\n",
     "    eval_rtc t v.\n",
     "\n",
     "Inductive full_eval : tm -> tm -> Prop :=\n",
     "| f_value : forall v,\n",
     "    value v ->\n",
     "    full_eval v v\n",
     "| f_iftrue : forall t1 t2 t3 v,\n",
     "    full_eval t1 tm_true ->\n",
     "    full_eval t2 v ->\n",
     "    full_eval (tm_if t1 t2 t3) v\n",
     "| f_iffalse : forall t1 t2 t3 v,\n",
     "    full_eval t1 tm_false ->\n",
     "    full_eval t3 v ->\n",
     "    full_eval (tm_if t1 t2 t3) v\n",
     "| f_succ : forall t v,\n",
     "    nvalue v ->\n",
     "    full_eval t v ->\n",
     "    full_eval (tm_succ t) (tm_succ v)\n",
     "| f_predzero : forall t,\n",
     "    full_eval t tm_zero ->\n",
     "    full_eval (tm_pred t) tm_zero\n",
     "| f_predsucc : forall t v,\n",
     "    nvalue v ->\n",
     "    full_eval t (tm_succ v) ->\n",
     "    full_eval (tm_pred t) v\n",
     "| f_iszerozero : forall t,\n",
     "    full_eval t tm_zero ->\n",
     "    full_eval (tm_iszero t) tm_true\n",
     "| f_iszerosucc : forall t v,\n",
     "    nvalue v ->\n",
     "    full_eval t (tm_succ v) ->\n",
     "    full_eval (tm_iszero t) tm_false.\n",
     "\n",
     "Lemma m_one_sol : forall t t',\n",
     "  eval t t' ->\n",
     "  eval_many t t'.\n",
     "Proof.\n",
     "  intros t t' He. apply m_step with (t' := t').\n",
     "    apply He.\n",
     "    apply m_refl.\n",
     "Qed.\n",
     "\n",
     "Lemma m_two_sol : forall t t' t'',\n",
     "  eval t t' ->\n",
     "  eval t' t'' ->\n",
     "  eval_many t t''.\n",
     "Proof.\n",
     "  intros t t' t'' He1 He2. apply m_step with (t' := t').\n",
     "    apply He1.\n",
     "    apply m_one. apply He2.\n",
     "Qed.\n",
     "\n",
     "Lemma m_iftrue_step_sol : forall t t1 t2 u,\n",
     "  eval t tm_true ->\n",
     "  eval_many t1 u ->\n",
     "  eval_many (tm_if t t1 t2) u.\n",
     "Proof.\n",
     "  intros t t1 t2 u He Hm.\n",
     "   apply m_step with (t' := tm_if tm_true t1 t2).\n",
     "    apply e_if. apply He.\n",
     "    apply m_step with (t' := t1).\n",
     "      apply e_iftrue.\n",
     "      apply Hm.\n",
     "Qed.\n",
     "\n",
     "Lemma m_if_iszero_conj_sol : forall v t2 t2' t3 t3',\n",
     "  nvalue v /\\ eval t2 t2' /\\ eval t3 t3' ->\n",
     "  eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\\\n",
     "  eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.\n",
     "Proof.\n",
     "  intros v t2 t2' t3 t3' H.\n",
     "   destruct H as [ Hn [ He1 He2 ] ]. split.\n",
     "    apply m_three with\n",
     "     (t' := tm_if tm_true t2 t3) (t'' := t2).\n",
     "      apply e_if. apply e_iszerozero.\n",
     "      apply e_iftrue.\n",
     "      apply He1.\n",
     "    apply m_three with\n",
     "     (t' := tm_if tm_false t2 t3) (t'' := t3).\n",
     "      apply e_if. apply e_iszerosucc. apply Hn.\n",
     "      apply e_iffalse.\n",
     "      apply He2.\n",
     "Qed.\n",
     "\n",
     "Lemma two_values_sol : forall t u,\n",
     "  value t /\\ value u ->\n",
     "    bvalue t \\/\n",
     "    bvalue u \\/\n",
     "    (nvalue t /\\ nvalue u).\n",
     "Proof.\n",
     "  unfold value. intros t u H.\n",
     "   destruct H as [ [ Hb1 | Hn1 ] H2 ].\n",
     "    left. apply Hb1.\n",
     "    destruct H2 as [ Hb2 | Hn2 ].\n",
     "      right. left. apply Hb2.\n",
     "      right. right. split.\n",
     "        apply Hn1.\n",
     "        apply Hn2.\n",
     "Qed.\n",
     "\n",
     "Lemma m_trans_sol : forall t u v,\n",
     "  eval_many t u ->\n",
     "  eval_many u v ->\n",
     "  eval_many t v.\n",
     "Proof.\n",
     "  intros t u v Hm1 Hm2. induction Hm1.\n",
     "    apply Hm2.\n",
     "    apply m_step with (t' := t').\n",
     "      apply H.\n",
     "      apply IHHm1. apply Hm2.\n",
     "Qed.\n",
     "\n",
     "Lemma eval_rtc_many_sol : forall t u,\n",
     "  eval_rtc t u ->\n",
     "  eval_many t u.\n",
     "Proof.\n",
     "  intros t u Hr. induction Hr.\n",
     "    apply m_one. apply H.\n",
     "    apply m_refl.\n",
     "    apply m_trans with (t' := u).\n",
     "      apply IHHr1.\n",
     "      apply IHHr2.\n",
     "Qed.\n",
     "\n",
     "Lemma eval_many_rtc_sol : forall t u,\n",
     "  eval_many t u ->\n",
     "  eval_rtc t u.\n",
     "Proof.\n",
     "  intros t u Hm. induction Hm.\n",
     "    apply r_refl.\n",
     "    apply r_trans with (u := t').\n",
     "      apply r_eval. apply H.\n",
     "      apply IHHm.\n",
     "Qed.\n",
     "\n",
     "Lemma full_eval_to_value_sol : forall t v,\n",
     "  full_eval t v ->\n",
     "  value v.\n",
     "Proof.\n",
     "  intros t v Hf. induction Hf.\n",
     "    apply H.\n",
     "    apply IHHf2.\n",
     "    apply IHHf2.\n",
     "    right. apply n_succ. apply H.\n",
     "    right. apply n_zero.\n",
     "    right. apply H.\n",
     "    left. apply b_true.\n",
     "    left. apply b_false.\n",
     "Qed."
    ]
   }
  ],
  "nbformat": 4,
  "nbformat_minor": 2,
  "metadata": {
   "language_info": {
    "name": "coq",
    "file_extension": ".v",
    "mimetype": "text/x-coq",
    "version": "8.9.1"
   },
   "kernelspec": {
    "name": "coq",
    "display_name": "Coq",
    "language": "coq"
   }
  }
 }
diff --git a/advanced.md b/advanced.md
index 0f4604a..2417e37 100644
--- a/advanced.md
+++ b/advanced.md
@@ -1,938 +1,932 @@
 ---
 title: My notebook
 jupyter:
   nbformat: 4
   nbformat_minor: 2
   kernelspec:
       display_name: "Coq"
       language: "coq"
       name: "coq"
   language_info:
       file_extension: ".v"
       mimetype: "text/x-coq"
       name: "coq"
       version: "8.9.1"
 ---
 
 Adapted from a workshop given at [POPL 2008](https://www.cis.upenn.edu/~plclub/popl08-tutorial/).
 
 # The NB language, back again
 
 In this notebook, we will be working with a language very similar to the NB
 language from the first assignment.
 
 ## Definitions
 ### Grammar and terms 
 
 The grammar of our language would be defined as follows:
 
 ```
 t  ::= "true"                   terms
      | "false"
      | "if" t "then" t "else" t
      | 0
      | "succ" t
      | "pred" t
      | "iszero" t
 ```
 
 To represent the terms of this language in Coq, we will define `tm`, an
 `Inductive` data type:
 
 ``` code
 Inductive tm : Set :=
 | tm_true : tm
 | tm_false : tm
 | tm_if : tm -> tm -> tm -> tm
 | tm_zero : tm
 | tm_succ : tm -> tm
 | tm_pred : tm -> tm
 | tm_iszero : tm -> tm.
 ```
 
 Compare the two definitions. For every rule in the grammar, there is a
 corresponding _constructor_. Each constructor is a value in Coq that allows us
 to obtain values of type `tm`. In contrast to the previous notebook, here we
 annotate every constructor with a type. `tm_true` is a constructor corresponding
 to the terminal rule `"true"` - it takes no arguments and is therefore annotated
 with the simple type `tm`. `tm_succ` is a constructor corresponding to the
 `"succ" t` rule - since the rule has a single subterm, the constructor is a
 function from `tm` to `tm`.
 
 Using the above definition, we can create values corresponding to the terms in our language:
 
 ```code
 (* Represents "if (iszero 0) false true" *)
 Check (tm_if (tm_iszero tm_zero) tm_false tm_true).
 ```
 
 ### Definition of value
 
 Next, we want to define what it means to be a _value_ in our language. While in
 the original NB language we did so through grammar rules, it's equally valid to
 define a judgment which tells us which terms are boolean and numeric values
 (correspondingly, `bvalue` and `nvalue`):
 
 ```
   ---------------  (b_true)
   ⊢ bvalue (true)
 
   ---------------- (b_false)
   ⊢ bvalue (false)
 
   
   ---------- (n_zero)
   ⊢ nvalue 0
   
      ⊢ nvalue t
   ----------------- (n_succ)
   ⊢ nvalue (succ t)
 ```
 
 Recall that from Curry-Howard correspondence we know that types correspond to
 propositions and values correspond to proofs. Therefore, we can represent the
 above judgements in Coq by defining types corresponding to the judgments. Those
 types are `bvalue t` and `nvalue t`. Being able to create a well-typed value of
 type `nvalue t` is the same as being able to construct a proof that a given term
 is an `nvalue`; same notion applies to  `bvalue t`.
 
 We define said types as follows:
 
 ```code
 Inductive bvalue : tm -> Prop := 
 | b_true : bvalue tm_true 
 | b_false : bvalue tm_false.
 
 Inductive nvalue : tm -> Prop :=
 | n_zero : nvalue tm_zero
 | n_succ : forall t,
     nvalue t ->
     nvalue (tm_succ t).
 ```
 
 Those definitions should look similar to the inference rules above, although
 they may also look slightly confusing. Before trying to understand their every
 part, it may help to see how they are meant to be used.
 
 Again, the _type_ `nvalue t` represents the _proposition_ that `t` is a numeric
 value. For instance, `nvalue (tm_succ tm_zero)` represents the proposition that
 the successor of zero (or simply one) is a numeric value. To show that this
 proposition is true, we need to construct a value of said type. We can do that
 as follows:
 
 ```code
 Check (n_succ tm_zero n_zero).
 ```
 
 You should now go back to the definitions and try to understand how they
 represent their corresponding inference rules.
 
 One thing that may still be puzzling are the `Set` and `tm -> Prop` annotation.
 If you are suspecting that the second one mentions `tm ->` because the
 corresponding type is a _type-level function_ from `tm` to `Prop`, you'd be correct:
 
 ```code
 Check nvalue.
 Check nvalue tm_zero.
 ```
 
 The difference between `Set` and `Prop` is much more subtle and fundamental. To
 put it briefly, types annotated as `Set` are meant to be used as data types,
 while those annotated as `Prop` are meant to be used as propositions. Fully
 explaining this distinction is beyond the scope of this course, but the above
 intuition should serve you well enough.
 
 As the last thing in this section, we will (finally) define what it means to be
 a value. If you recall that `T \/ S` is the data type corresponding to the
 proof that either `T` or `S`, the definition is simple enough:
 
 ```code
-Inductive value : t -> Prop :=
-| v_bvalue : forall t,
-    bvalue t ->
-    value t
-| v_nvalue : forall t,
-    nvalue t ->
-    value t
+Definition value (t : tm) : Prop :=
+  bvalue t \/ nvalue t.
 ```
-
 ### Operational semantics
 
 Having defined `tm`s and `value`s, we can define call-by-value operational
 semantics for our language. We will define an inductive data type `eval (t : tm)
 (t' : tm) : Prop` corresponding to the proposition that `t` evaluates to `t'` in
 a single step. The definition is as follows:
 
 ```code
 Inductive eval : tm -> tm -> Prop :=
 | e_iftrue : forall t2 t3,
     eval (tm_if tm_true t2 t3) t2
 | e_iffalse : forall t2 t3,
     eval (tm_if tm_false t2 t3) t3
 | e_if : forall t1 t1' t2 t3,
     eval t1 t1' ->
     eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)
 | e_succ : forall t t',
     eval t t' ->
     eval (tm_succ t) (tm_succ t')
 | e_predzero :
     eval (tm_pred tm_zero) tm_zero
 | e_predsucc : forall t,
     nvalue t ->
     eval (tm_pred (tm_succ t)) t
 | e_pred : forall t t',
     eval t t' ->
     eval (tm_pred t) (tm_pred t')
 | e_iszerozero :
     eval (tm_iszero tm_zero) tm_true
 | e_iszerosucc : forall t,
     nvalue t ->
     eval (tm_iszero (tm_succ t)) tm_false
 | e_iszero : forall t t',
     eval t t' ->
     eval (tm_iszero t) (tm_iszero t').
 ```
 
 If you don't feel comfortable with Coq syntax yet, compare the above with the
 definition of beta-reduction from our first assignment.
 
 Next, we define the multi-step evaluation relation `eval_many`, corresponding to multi-step beta-reduction.
 
 Its inference rules are:
 
 ```
  -------------  (m_refl)
  eval_many t t 
  
  eval t t'    eval_many t' u
  ---------------------------  (m_step)
        eval_many t u
 ```
 
 And its definition is:
 
 ```code
 Inductive eval_many : tm -> tm -> Prop :=
 | m_refl : forall t,
     eval_many t t
 | m_step : forall t t' u,
     eval t t' ->
     eval_many t' u ->
     eval_many t u.
 ```
 
 ### Exercises
 
 **Note** The exercises below may be hard. If you find yourself stuck when doing
 them, copy the definitions from solutions here - they will be useful later on.
 
 **Exercise** Multi-step evaluation is often defined as the "reflexive,
 transitive closure" of single-step evaluation. Write an inductively defined
 relation `eval_rtc` that corresponds to that verbal description.
 
 In case you get stuck or need a hint, you can find solutions to all the
 exercises near the bottom of the file.
  
 **Exercise** Sometimes it is more convenient to use a big-step semantics for a
 language. Add the remaining constructors to finish the inductive definition
 `full_eval` for the big-step semantics that corresponds to the small-step
 semantics defined by `eval`. Build the inference rules so that `full_eval t v`
 logically implies both `eval_many t v` and `value v`. In order to do this, you
 may need to add the premise `nvalue v` to the appropriate cases.
 
 Hint: You should end up with a total of 8 cases.
 
 ```
 Inductive full_eval : tm -> tm -> Prop :=
 | f_value : forall v,
     value v ->
     full_eval v v
 | f_iftrue : forall t1 t2 t3 v,
     full_eval t1 tm_true ->
     full_eval t2 v ->
     full_eval (tm_if t1 t2 t3) v
 | f_succ : forall t v,
     nvalue v ->
     full_eval t v ->
     full_eval (tm_succ t) (tm_succ v).
 ```
 
 ## Proofs
 
 So far, we've only seen proofs represented in Coq as manually-constructed
 values. For any non-trivial proof value, it's rather inconvenient to manually
 construct it.
 
 Proof values are most easily built interactively, using tactics to manipulate a
 proof state. A proof state consists of a set of goals (propositions or types for
 which you must produce an inhabitant), each with a context of hypotheses
 (inhabitants of propositions or types you are allowed to use). A proof state
 begins initially with one goal (the statement of the lemma you are trying to
 prove) and no hypotheses. A goal can be solved, and thereby eliminated, when it
 exactly matches one of hypotheses in the context. A proof is completed when all
 goals are solved.
 
 Tactics can be used for forward reasoning (which, roughly speaking, means
 modifying the hypotheses of a context while leaving the goal unchanged) or
 backward reasoning (replacing the current goal with one or more new goals in
 simpler contexts). Given the level of detail required in a formal proof, it
 would be ridiculously impractical to complete a proof using forward reasoning
 alone. However it is usually both possible and practical to complete a proof
 using backward reasoning alone. Therefore, we focus almost exclusively on
 backward reasoning in this tutorial. Of course, most people naturally use a
 significant amount of forward reasoning in their thinking process, so it may
 take you a while to become accustomed to getting by without it.
 
 We use the keyword `Lemma` to state a new proposition we wish to prove.
 (`Theorem` and `Fact` are exact synonyms for `Lemma`.) The keyword `Proof`,
 immediately following the statement of the proposition, indicates the beginning
 of a proof script. A proof script is a sequence of tactic expressions, each
 concluding with a `.`. Once all of the goals are solved, we use the keyword
 `Qed` to record the completed proof. If the proof is incomplete, we may tell Coq
 to accept the lemma on faith by using `Admitted` instead of `Qed`.
 
 We now proceed to introduce the specific proof tactics.
 
 ### Implication and universal quantification
 
 ```
     - [intros]
     - [apply]
     - [apply with (x := ...)]
 ```
 
 Recall that both implication and universal quantification correspond to function
 types and values. Accordingly, we can use the `intros` tactic to move
 universally quantified variables and implication antecedents from the goal into
 the context as hypotheses.
 
 If our current goal corresponds to a conclusion of some implication `P`, we can
 use the `apply P` tactic to prove our goal by proving the antecedents of `P`. If
 you'd suspect from the name of the tactic that this corresponds to applying a
 function, you'd be correct. Using `apply` allows building a proof value from the
 bottom up.
 
 #### Example 1
 
 In the following example, we will create a value corresponding to a (still)
 simple proposition. Step through every cell below to see how this value is
 constructed.
 
 ```code
 Lemma e_succ_pred_succ : forall t,
   nvalue t ->
   eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t).
 Proof.
 ```
 
 ```code
   (** Let [t] be a [tm]. *)
   intros t.
 ```
 
 ```code
   (** Assume that [t] is an [nvalue] (and let's call that
       assumption [Hn] for future reference). *)
   intros Hn.
 ```
 
 ```code
   (** By [e_succ], in order to prove our conclusion, it suffices
       to prove that [eval (tm_pred (tm_succ t)) t]. *)
   Check e_succ.
   apply e_succ.
 ```
 
 ```code
   (** That, in turn, can be shown by [e_predsucc], if we are
       able to show that [nvalue t]. *)
   Check e_predsucc.
   apply e_predsucc.
 ```
 
 ```code
   (** But, in fact, we assumed [nvalue t]. *)
   apply Hn.
 ```
 
 ``` code
 Qed.
 ```
 
 At this point, we have successfully concluded our proof; `e_succ_pred_succ` is a
 value that can be used like any other value we have seen so far. It corresponds
 to the following proof tree:
 
 ```
                         nvalue t
              ---------------------------- (e_predsucc)
              eval (tm_pred (tm_succ t)) t
     ------------------------------------------------ (e_succ)
     eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)
 ```
 
 We can see the value we have constructed with the following command:
 
 ```code
 Print e_succ_pred_succ.
 ```
 
 Compare the value to the proof script above. Observe how function application in
 the value corresponds to usages of `apply` tactic.
 
 #### Example 2
 
 Now consider, for a moment, the rule `m_step`:
 
 ```
     eval t t'  eval_many t' u
     ------------------------- (m_step)
           eval_many t u
 ```
 
 If we have a goal such as `eval_many e1 e2`, we should be able to use `apply
 m_step` in order to replace it with the goals `eval e1 t'` and `eval_many t'
 e2`. But what exactly is `t'` here? When and how is it chosen? It stands to
 reason the conclusion is justified if we can come up with any `t'` for which the
 premises can be justified.
 
 Now we note that, in the Coq syntax for the type of `m_step`, all three
 variables `t`, `t'`, and `u` are universally quantified. The tactic `apply
 m_step` will use pattern matching between our goal and the conclusion of
 `m_step` to find the only possible instantiation of `t` and `u`. However, `apply
 m_step` will raise an error since it does not know how it should instantiate
 `t'`. In this case, the `apply` tactic takes a `with` clause that allows us to
 provide this instantiation. This is demonstrated in the proof below. 
 
 Observe how this works in the proof script below. The proof tree here gives a
 visual representation of the proof term we are going to construct and the proof
 script has again been annotated with the steps in English.
 
 ```
     Letting   s = tm_succ
               p = tm_pred
             lem = e_succ_pred_succ,
 
             nvalue t
     - - - - - - - - - - - - (lem)    --------------------- (m_refl)
     eval (s (p (s t))) (s t)         eval_many (s t) (s t)
     ------------------------------------------------------ (m_step)
                   eval_many (s (p (s t))) (s t)
 ```
 
 ``` code
 Lemma m_succ_pred_succ : forall t,
   nvalue t ->
   eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).
 Proof.
 ```
 
 ```code
   (** Let [t] be a [tm], and assume [nvalue t]. *)
   intros t Hn.
 ```
 
 ```code
   (** By [m_step], to show our conclusion, it suffices to find
       some [t'] for which
         [eval (tm_succ (tm_pred (tm_succ t))) t']
       and
         [eval t' (tm_succ t)].
       Let us choose [t'] to be [tm_succ t]. *)
   Check m_step.
   apply m_step with (t' := tm_succ t).
 ```
 
 ```code
     (** By the lemma [e_succ_pred_succ], to show
           [eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)],
         it suffices to show [nvalue t]. *)
     Check e_succ_pred_succ.
     apply e_succ_pred_succ.
 ```
 
 ```code
     (** And, in fact, we assumed [nvalue t]. *)
     apply Hn.
 ```
 
 ```code
     (** Moreover, by the rule [m_refl], we also may conclude
         [eval (tm_succ t) (tm_succ t)]. *)
     Check m_refl.
     apply m_refl.
 ```
 
 ```code
 Qed.
 ```
 
 #### Lab 1
 
 Write proof scripts for the following lemmas, following the plain language descriptions.
 
 These lemmas will be useful in later proofs.
 
 ``` code
 Lemma m_one : forall t1 t2,
   eval t1 t2 ->
   eval_many t1 t2.
 ```
 
 ```code
   (** Let [t1] and [t2] be terms, and assume [eval t1 t2].  We
       may conclude [eval_many t1 t2] by [m_step] if we can find
       a term [t'] such that [eval t1 t'] and [eval_many t' t2].
       We will choose [t'] to be [t2].  Now we can show
       [eval t1 t2] by our assumption, and we can show
       [eval_many t2 t2] by [m_refl]. *)
 Proof.
 ```
 
 ```code
   (* to finish *)
 Admitted.
 ```
 
 ``` code
 Lemma m_two : forall t1 t2 t3,
   eval t1 t2 ->
   eval t2 t3 ->
   eval_many t1 t3.
 ```
 
 ```code
   (** Let [t1], [t2], and [t3] be terms.  Assume [eval t1 t2]
       and [eval t2 t3].  By [m_step], we may conclude that
       [eval_many t1 t3] if we can find a term [t'] such that
       [eval t1 t'] and [eval_many t' t3].  Let's choose [t'] to
       be [t2].  We know [eval t1 t2] holds by assumption.  In
       the other case, by the lemma [m_one], to show [eval_many
       t2 t3], it suffices to show [eval t2 t3], which is one of
       our assumptions.  *)
 Proof.
 ```
 
 ```code
   (* to finish *)
 Admitted.
 ```
 
 ```code
 Lemma m_iftrue_step : forall t t1 t2 u,
   eval t tm_true ->
   eval_many t1 u ->
   eval_many (tm_if t t1 t2) u.
 ```
 
 ```code
   (** Let [t], [t1], [t2], and [u] be terms.  Assume that
       [eval t tm_true] and [eval_many t1 u].  To show
       [eval_many (tm_if t t1 t2) u], by [m_step], it suffices to
       find a [t'] for which [eval (tm_if t t1 t2) t'] and
       [eval_many t' u].  Let us choose [t'] to be
       [tm_if tm_true t1 t2].  Now we can use [e_if] to show that
       [eval (tm_if t t1 t2) (tm_if tm_true t1 t2)] if we can
       show [eval t tm_true], which is actually one of our
       assumptions.  Moreover, using [m_step] once more, we can
       show [eval_many (tm_if tm_true t1 t2) u] where [t'] is
       chosen to be [t1].  Doing so leaves us to show
       [eval (tm_if tm_true t1 t2) t1] and [eval_many t1 u].  The
       former holds by [e_iftrue] and the latter holds by
       assumption. *)
 Proof.
 ```
 
 ```code
   (* to finish *)
 Admitted.
 ```
 
 ### Working with Conjunction and Disjunction
 
 ```
     - [split]
     - [left]
     - [right]
     - [destruct] (for conjunction and disjunction)
 ```
 
 **Example** If `H` is the name of a conjunctive hypothesis, then `destruct H as p` will
 replace the hypothesis `H` with its components using the names in the pattern
 `p`. Observe the pattern in the example below.
 
 ``` code
 Lemma m_two_conj : forall t t' t'',
   eval t t' /\ eval t' t'' ->
   eval_many t t''.
 Proof.
   intros t t' t'' H.
    destruct H as [ He1 He2 ].
    apply m_two with (t2 := t').
     apply He1.
     apply He2.
 Qed.
 ```
 
 **Example** Patterns may be nested to break apart nested structures. Note that
 infix conjunction is right-associative, which is significant when trying to
 write nested patterns. We will later see how to use `destruct` on many different
 sorts of hypotheses.
  
 ``` code
 Lemma m_three_conj : forall t t' t'' t''',
   eval t t' /\ eval t' t'' /\ eval t'' t''' ->
   eval_many t t'''.
 Proof.
   intros t t' t'' t''' H.
    destruct H as [ He1 [ He2 He3 ] ].
    apply m_step with (t' := t').
     apply He1.
     apply m_two with (t2 := t'').
       apply He2.
       apply He3.
 Qed.
 ```
 
 **Example** If your goal is a conjunction, use `split` to break it apart into
 two separate subgoals.
  
 ``` code
 Lemma m_three : forall t t' t'' t''',
   eval t t' ->
   eval t' t'' ->
   eval t'' t''' ->
   eval_many t t'''.
 Proof.
   intros t t' t'' t''' He1 He2 He3.
    apply m_three_conj with (t' := t') (t'' := t'').
     split.
       apply He1.
       split.
         apply He2.
         apply He3.
 Qed.
 ```
 
 **Exercise** Hint: You might find lemma `m_three` useful here.
  
 ``` code
 Lemma m_if_iszero_conj : forall v t2 t2' t3 t3',
   nvalue v /\ eval t2 t2' /\ eval t3 t3' ->
   eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\
   eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.
 Proof.
 ```
 
 ```code
   (* to finish *)
 Admitted.
 ```
 
 **Example** If we have a disjunction in the context, we can use `destruct` to
 reason by cases on the hypothesis. Note the syntax of the associated pattern.
  
 ``` code
 Lemma e_if_true_or_false : forall t1 t2,
   eval t1 tm_true \/ eval t1 tm_false ->
   eval_many (tm_if t1 t2 t2) t2.
 Proof.
   intros t1 t2 H. destruct H as [ He1 | He2 ].
     apply m_two with (t2 := tm_if tm_true t2 t2).
       apply e_if. apply He1.
       apply e_iftrue.
     apply m_two with (t2 := tm_if tm_false t2 t2).
       apply e_if. apply He2.
       apply e_iffalse.
 Qed.
 ```
 
 ## Reasoning by Cases and Induction
 
 ```
     - [destruct] (for inductively defined propositions)
     - [induction]
 ```
 
 **Example** Use `destruct` to reason by cases on an inductively defined datatype
 or proposition.
 
 ``` code
 Lemma e_iszero_nvalue : forall v,
   nvalue v ->
   eval (tm_iszero v) tm_true \/
   eval (tm_iszero v) tm_false.
 Proof.
   intros v Hn.
 ```
 
 ```code
   destruct Hn.
 ```
 
 ```code
   (* Case [n_zero].
      Note how [v] becomes [tm_zero] in the goal. *)
     left.
 ```
 
 ```code
     apply e_iszerozero.
 ```
 
 ```code
   (* Case [n_succ].
      Note how [v] becomes [tm_succ v] in the goal. *)
     right.
 ```
 
 ``` code
     apply e_iszerosucc. apply Hn.
 Qed.
 ```
 
 **Example** You can use `induction` to reason by induction on an inductively
 defined datatype or proposition. This is the same as `destruct`, except that it
 also introduces an induction hypothesis in the inductive cases.
  
 ``` code
 Lemma m_iszero : forall t u,
   eval_many t u ->
   eval_many (tm_iszero t) (tm_iszero u).
 Proof.
   intros t u Hm. induction Hm.
     apply m_refl.
     apply m_step with (t' := tm_iszero t').
       apply e_iszero. apply H.
       apply IHHm.
 Qed.
 ```
 
 #### Lab 3
 Work on the following exercise.
 
 **Exercise** 
 
 ``` code
 Lemma m_trans : forall t t' u,
   eval_many t t' ->
   eval_many t' u ->
   eval_many t u.
 ```
 
 ```code
   (** We proceed by induction on the derivation of
       [eval_many t t'].
       Case [m_refl]: Since [t] and [t'] must be the same, our
         conclusion holds by assumption.
       Case [m_step]: Now let's rename the [t'] from the lemma
         statement to [u0] (as Coq likely will) and observe that
         there must be some [t'] (from above the line of the
         [m_step] rule) such that [eval t t'] and
         [eval_many t' u0].  Our conclusion follows from from
         an application of [m_step] with our new [t'] and our
         induction hypothesis, which allows us to piece together
         [eval_many t' u0] and [eval_many u0 u] to get
         [eval_many t' u]. *)
 Proof.
 ```
 
 ```code
   (* to finish *)
 Admitted.
 ```
 
 **Exercise** Prove the following lemma.
 
 Hint: You may be interested in some previously proved lemmas, such as `m_one`
 and `m_trans`.
 
 Note: Even though this lemma is in a comment, its solution is also at the
 bottom. (Coq will give an error if we leave it uncommented since it mentions the
 `eval_rtc` relation, which was the solution to another exercise.)
 
 ```
 Lemma eval_rtc_many : forall t u,
   eval_rtc t u ->
   eval_many t u.
 ```
 
 **Exercise** Prove the following lemma.
 
 ```
 Lemma eval_many_rtc : forall t u,
   eval_many t u ->
   eval_rtc t u.
 ```
 
 
 **Exercise** Prove the following lemma.
 
 ```
 Lemma full_eval_to_value : forall t v,
   full_eval t v ->
   value v.
 ```
 
 # Solutions to Exercises
 
 ``` code
 Inductive eval_rtc : tm -> tm -> Prop :=
 | r_eval : forall t t',
     eval t t' ->
     eval_rtc t t'
 | r_refl : forall t,
     eval_rtc t t
 | r_trans : forall t u v,
     eval_rtc t u ->
     eval_rtc u v ->
     eval_rtc t v.
 
 Inductive full_eval : tm -> tm -> Prop :=
 | f_value : forall v,
     value v ->
     full_eval v v
 | f_iftrue : forall t1 t2 t3 v,
     full_eval t1 tm_true ->
     full_eval t2 v ->
     full_eval (tm_if t1 t2 t3) v
 | f_iffalse : forall t1 t2 t3 v,
     full_eval t1 tm_false ->
     full_eval t3 v ->
     full_eval (tm_if t1 t2 t3) v
 | f_succ : forall t v,
     nvalue v ->
     full_eval t v ->
     full_eval (tm_succ t) (tm_succ v)
 | f_predzero : forall t,
     full_eval t tm_zero ->
     full_eval (tm_pred t) tm_zero
 | f_predsucc : forall t v,
     nvalue v ->
     full_eval t (tm_succ v) ->
     full_eval (tm_pred t) v
 | f_iszerozero : forall t,
     full_eval t tm_zero ->
     full_eval (tm_iszero t) tm_true
 | f_iszerosucc : forall t v,
     nvalue v ->
     full_eval t (tm_succ v) ->
     full_eval (tm_iszero t) tm_false.
 
 Lemma m_one_sol : forall t t',
   eval t t' ->
   eval_many t t'.
 Proof.
   intros t t' He. apply m_step with (t' := t').
     apply He.
     apply m_refl.
 Qed.
 
 Lemma m_two_sol : forall t t' t'',
   eval t t' ->
   eval t' t'' ->
   eval_many t t''.
 Proof.
   intros t t' t'' He1 He2. apply m_step with (t' := t').
     apply He1.
     apply m_one. apply He2.
 Qed.
 
 Lemma m_iftrue_step_sol : forall t t1 t2 u,
   eval t tm_true ->
   eval_many t1 u ->
   eval_many (tm_if t t1 t2) u.
 Proof.
   intros t t1 t2 u He Hm.
    apply m_step with (t' := tm_if tm_true t1 t2).
     apply e_if. apply He.
     apply m_step with (t' := t1).
       apply e_iftrue.
       apply Hm.
 Qed.
 
 Lemma m_if_iszero_conj_sol : forall v t2 t2' t3 t3',
   nvalue v /\ eval t2 t2' /\ eval t3 t3' ->
   eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\
   eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.
 Proof.
   intros v t2 t2' t3 t3' H.
    destruct H as [ Hn [ He1 He2 ] ]. split.
     apply m_three with
      (t' := tm_if tm_true t2 t3) (t'' := t2).
       apply e_if. apply e_iszerozero.
       apply e_iftrue.
       apply He1.
     apply m_three with
      (t' := tm_if tm_false t2 t3) (t'' := t3).
       apply e_if. apply e_iszerosucc. apply Hn.
       apply e_iffalse.
       apply He2.
 Qed.
 
 Lemma two_values_sol : forall t u,
   value t /\ value u ->
     bvalue t \/
     bvalue u \/
     (nvalue t /\ nvalue u).
 Proof.
   unfold value. intros t u H.
    destruct H as [ [ Hb1 | Hn1 ] H2 ].
     left. apply Hb1.
     destruct H2 as [ Hb2 | Hn2 ].
       right. left. apply Hb2.
       right. right. split.
         apply Hn1.
         apply Hn2.
 Qed.
 
 Lemma m_trans_sol : forall t u v,
   eval_many t u ->
   eval_many u v ->
   eval_many t v.
 Proof.
   intros t u v Hm1 Hm2. induction Hm1.
     apply Hm2.
     apply m_step with (t' := t').
       apply H.
       apply IHHm1. apply Hm2.
 Qed.
 
 Lemma eval_rtc_many_sol : forall t u,
   eval_rtc t u ->
   eval_many t u.
 Proof.
   intros t u Hr. induction Hr.
     apply m_one. apply H.
     apply m_refl.
     apply m_trans with (t' := u).
       apply IHHr1.
       apply IHHr2.
 Qed.
 
 Lemma eval_many_rtc_sol : forall t u,
   eval_many t u ->
   eval_rtc t u.
 Proof.
   intros t u Hm. induction Hm.
     apply r_refl.
     apply r_trans with (u := t').
       apply r_eval. apply H.
       apply IHHm.
 Qed.
 
 Lemma full_eval_to_value_sol : forall t v,
   full_eval t v ->
   value v.
 Proof.
   intros t v Hf. induction Hf.
     apply H.
     apply IHHf2.
     apply IHHf2.
     right. apply n_succ. apply H.
     right. apply n_zero.
     right. apply H.
     left. apply b_true.
     left. apply b_false.
 Qed.
 ```