In this walkthrough you will learn...

• How to use lemmas
• How to state and use definitions

# Introduction

This advanced walkthrough assumes you have finished the beginner's walkthrough and are familiar with the following tactics: `induction`, `intros`, `case`, `apply`, and `search`.

This walkthrough is concerned with the simply-typed lambda calculus. Simple types are those constructed starting from base types using the function type constructor; the main difference between these types and those considered in the earlier walkthrough is that the language of types now does not include type variables. At the level of terms, another difference is that the atoms are assumed to have specific types at the beginning. We are interested in terms that are constructed only using applications and abstractions and so the type for atoms (that are only the abstracted variables) is given by including a type with each abstraction. Typing rules allow us to assign types to more complicated expressions. These rules look very much like the ones in the beginner's walkthrough with the only difference that the rule for abstractions has to use the provided type for the abstracted variable. The property that we will prove is that in such a case there is exactly one type that can be assigned to each well-formed term.

# Executable Specification

This walkthrough uses the following signature which we assume is saved in `type-uniq.sig`.

```sig type-uniq.

kind    tm, ty     type.

type    i          ty.
type    arrow      ty -> ty -> ty.

type    app        tm -> tm -> tm.
type    abs        ty -> (tm -> tm) -> tm.

type    of         tm -> ty -> o.
```

Note that this signature differs from signature in the first walkthrough in that the `abs` constructor now takes two arguments, the first of which is the type of the variable which is abstracted over.

The specification of typing in the simply-typed lambda-calculus are specified in the following module which we assume is saved in `type-uniq.mod`.

```module type-uniq.

of (abs T R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.
```

Note that the rule for typing abstractions uses the type annotation which is attached to each abstraction.

# Reasoning

The specification is already included with Abella in the directory `examples/lambda-calculus/type-uniq` as the files `type-uniq.sig` and `type-uniq.mod`. We can load this specification in Abella as follows.

```~/abella/examples/lambda-calculus/type-uniq % abella
Welcome to Abella 2.0.0
Abella < Specification "type-uniq".

Abella <
```
We state our type uniqueness theorem as follows.
```Abella < Theorem type_uniq : forall E T1 T2,
{of E T1} -> {of E T2} -> T1 = T2.
```
We will induct on the height of `{of E T1}`, use `intros`, and then do case analysis on ```{of E T1}```. This results in two subgoals corresponding to the two specification rules for `of`. The first subgoal is when `E` is an abstraction; the second subgoal is abbreviated for now.
```Subgoal 1:

Variables: E, T1, T2, U, R, T
IH : forall E T1 T2, {of E T1}* -> {of E T2} -> T1 = T2
H2 : {of (abs T R) T2}
H3 : {of n1 T |- of (R n1) U}*
============================
arrow T U = T2

Subgoal 2 is:
T1 = T2
```
At this point `E` has been bound to `(abs T R)`. There is only one way in which `{of (abs T R) T2}` can be derived, thus case analysis on this hypothesis acts like unfolding this judgment. The result is as follows.
```Subgoal 1:

Variables: E, T1, T2, U, R, T, U1
IH : forall E T1 T2, {of E T1}* -> {of E T2} -> T1 = T2
H3 : {of n1 T |- of (R n1) U}*
H4 : {of n1 T |- of (R n1) U1}
============================
arrow T U = arrow T U1

Subgoal 2 is:
T1 = T2
```
It looks like we are almost there, but something goes wrong when we try to apply the inductive hypothesis to ```{of n1 T |- of (R n1) U}*``` and `{of n1 T |- of (R n1) U1}`.
```type_uniq < apply IH to H3 H4.
Error:  Contexts did not match
```

Basically what happened is that our theorem was stated for typing judgments that have an empty context of hypothetical assumptions. We can think of `{of E T1}` as being `{nil |- of E T1}`. When we tried to apply our inductive hypothesis to judgments which had non-empty contexts, it failed. The problem is that we need to generalize our theorem over the possible contexts in which typing judgments are made. Roughly we want something like the following.

``` forall L E T1 T2, {L |- of E T1} -> {L |- of E T2} -> T1 = T2. ```
However, this statement is too general and, in fact, not true. To begin with, we are not interested in it being true for all `L`, only for those `L`s that assign types to terms. Moreover, the relevant `L`s should assign types only to nominal constants (which represent abstracted variables in the proof) and at most one type to each such constant. Notice that without this uniqueness assumption about the assignment of types to variables, the proposition cannot be true.

The way we will realize this restriction is by defining a property called `ctx` that we expect all good contexts to satisfy and then requiring this property to hold of `L` in the statement of the theorem. If you are following this walkthrough in Abella, you first need to type "`abort.`" to give up on our previous proof attempt. Then enter the following definition of `ctx`.

```Define ctx : olist -> prop by
ctx nil ;
nabla x, ctx (of x T :: L) := ctx L.
```

The system should accept this command with no output. What this definition says is that the empty list is well-formed context and the list `(of x T :: L)` is a well-formed context if `x` is a nominal constant and `L` is a well-formed context; here `nil` represents the empty list and `::` is a built-in infix constructor for lists. When we define `ctx` here we also give it a type which is `olist -> prop`, where `olist` is the type of lists of terms of type `o` and `prop` is the type of formulas in the reasoning logic.

The definition of `ctx` ensures that the following atomic formula is provable in the reasoning logic

``` ctx (of n1 T1 :: of n2 T2 :: of n3 T3 :: nil) ```
where `n1`, `n2`, and `n3` are nominal constants. This definition also ensures that the following formulas are not provable.
``` ctx (of n1 T1 :: of n1 T2 :: nil) ```
``` ctx (of (app M N) T :: nil) ```
``` ctx (of (abs R) T :: nil) ```

These non-examples illustrate facts that we would like to prove about well-formed contexts. The first is that they cannot contain more than one typing judgment for the same nominal constant. In proving this lemma, we will need another fact about the non-occurrence of nominal constants with a particular kind of scope in a list. This property can be stated using the predicate `member` that is known to Abella via the following definition. Do not type this in, since this is already defined in Abella.

```Define member : o -> olist -> prop by
member A (A :: L) ;
member A (B :: L) := member A L.
```
The property we need is stated in the following lemma:
```Theorem member_nominal_absurd : forall L T, nabla x,
member (of x T) L -> false.
```
Before we consider a proof of this lemma, it is useful to consider the following simpler observation that is in some ways related:
```Theorem non_occurrence : forall L, nabla (x:tm),
(x = L) -> false.
```
The particular order in which the quantifiers over `L` and `x` are scoped automatically enforces the requirement that any nominal constant substituted for `x` cannot appear in the term substituted for `L`. Abella understands this and this theorem is therefore easily proved. In detail, the proof will follow quickly by using the tactics `intros` and `case H1`.

Given that non_occurrence is provable, one might wonder if member_nominal_absurd does not follow immediately from it: the property is after all similar in that we are trying to show the non-occurrence of the nominal constant plugged in for `x` in the statement of member_nominal_absurd in the term substituted for `L`. Unfortunately, this is not true. `L` is a list that is, in a sense, constructed using the definition of `member` and we have to factor this non-occurrence property through that definition.

Once we have observed this much, the actual proof is easy to perform and so I'll just show it.

```

============================
forall L T, nabla x, member (of x T) L -> false

member_nominal_absurd < induction on 1.
```
```

IH : forall L T, nabla x, member (of x T) L * -> false
============================
forall L T, nabla x, member (of x T) L @ -> false

member_nominal_absurd < intros.
```
```
Variables: L, T
IH : forall L T, nabla x, member (of x T) L * -> false
H1 : member (of n1 T) L @
============================
false

member_nominal_absurd < case H1.
```
```
Variables: L, T, L3, L2
IH : forall L T, nabla x, member (of x T) L * -> false
H2 : member (of n1 T) L3 *
============================
false

member_nominal_absurd < apply IH to H2.
Proof completed.
```
The interesting part is when we did `case H1` we didn't have to consider the subgoal when `(of n1 T)` is at the head of `L`. Here the fact that the instantiation of `L` cannot contain `n1`, the nominal constant substituted for `x`, gets used.

If we now attempt to prove the uniqueness property for contexts we will still run into a small problem: we will encounter terms of the form `T n1` where `T` is a variable of type `ty` and `n1` is a nominal constant of type `tm`. Such terms are absurd since it is not possible for a term of type `tm` to appear inside a term of type `ty`. Abella does not know this, however, since the user may later add a new constant with type `tm -> ty` which would allow such dependencies. In order to let Abella know that such constants will never be introduced, we tell it that the types `tm` and `ty` are closed using the following command:

`Close tm, ty.`

Now we can now state and prove the uniqueness property for contexts.

```Theorem ctx_uniq : forall L E T1 T2,
ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.
```
This lemma can be proved by induction on any of the hypotheses. We will induct on `member (of E T1) L` followed by `intros` and case analysis on ```member (of E T1) L```. This results in two subgoals based on whether ```(of E T1)``` occurs in the head or the tail of `L`. The proof state is as follows.
```Subgoal 1:

Variables: L, E, T1, T2, L1
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H1 : ctx (of E T1 :: L1)
H3 : member (of E T2) (of E T1 :: L1)
============================
T1 = T2

Subgoal 2 is:
T1 = T2
```
The first subgoal is when `(of E T1)` is at the head of `L` which is therefore `(of E T1 :: L1)`. Next we do case analysis on `member (of E T2) (of E T1 :: L1)` which will replace the current subgoal with two new subgoals, bringing the total number of subgoals to three. The first subgoal will be when `(of E T2)` is at the head of the list. This means `T1 = T2` so the subgoal is trivially handled by `search.` After this, two subgoals remain.
```Subgoal 1.2:

Variables: L, E, T1, T2, L1
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H1 : ctx (of E T1 :: L1)
H4 : member (of E T2) L1
============================
T1 = T2

Subgoal 2 is:
T1 = T2
```
Let's stop to think about the first subgoal. It is stating that `(of E T1 :: L1)` is a well-formed typing context and yet there is another binding for `E` in `L1`. This is a contradiction and we need to expose it to the prover.

Here we perform case analysis on `ctx (of E T1 :: L1)`. This case analysis will be interesting because the `ctx` was defined with a nabla quantifier in the head of the definition. As a reminder, here is the relevant definition of `ctx`. Don't type this in again, it is only to remind you.

```  nabla x, ctx (of x T :: L) := ctx L
```
Based on the intended meaning of this clause that we discussed earlier, ```ctx (of E T1 :: L1)``` can follow from it only if `E` is a nominal constant and `T1` and `L1` are restricted to be terms that do not contain this nominal constant. The logical form of the unfolding rule is treated in detail in this paper. The effect of this rule on the existing proof state will be to introduce a new nominal constant for `E` and to require that the newly introduced eigenvariables not contain this constant. Of course, the previously available eigenvariables can use the nominal constant. To resolve this seemingly contradictory requirements, we stipulate that no eigenvariable can be instantiated by a term containing a nominal constant but we also replace the original eigenvariables by new ones applied to the introduced nominal constant. This mechanism, that is known technically as raising, allows dependencies to be represented even under the restriction on substitutions for eigenvariables. In the current case, however, the nominal constant we are raising over has type `tm` and the only eigenvariables we might have to raise are of type `ty`. Since we used the `Close` command, Abella knows that the `ty` variables cannot depend on terms of type `tm`, and thus no raising is performed.

Effecting an unfolding in the manner described in the current situation yields the following as the new proof state.

```ctx_uniq < case H1.
Subgoal 1.2:

Variables: L, E, T1, T2, L1, L2
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H4 : member (of n1 T2) L2
H5 : ctx L2
============================
T1 = T2

Subgoal 2 is:
T1 = T2
```
We can complete this subgoal by applying our lemma about occurrences of nominal constants.
```ctx_uniq < apply member_nominal_absurd to H4.
```
This completes the subgoal and leaves just the following subgoal left to be proven.
```Subgoal 2:

Variables: L, E, T1, T2, L1, B
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H1 : ctx (B :: L1)
H3 : member (of E T2) (B :: L1)
H4 : member (of E T1) L1 *
============================
T1 = T2
```
Now we perform case analysis on ```member (of E T2) (B :: L1)``` which generates two subgoals. The first subgoal is symmetric to the previous subgoal we considered, so I'll leave that for you. The other subgoal is as follows.
```Subgoal 2.2:

Variables: L, E, T1, T2, L1, B
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H1 : ctx (B :: L1)
H4 : member (of E T1) L1 *
H5 : member (of E T2) L1
============================
T1 = T2
```
All we need now to apply the inductive hypothesis is a judgment like `ctx L1`. We get this by case analysis which triggers raising of eigenvariables; this raising which is shown in the prover state below ends up having no effect on the proof itself. The rest of the proof is, in fact, as follows.
```ctx_uniq < case H1.
Subgoal 2.2:

Variables: L, E, T1, T2, L1, B, L2, T
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H4 : member (of (E n1) T1) L2 *
H5 : member (of (E n1) T2) L2
H6 : ctx L2
============================
T1 = T2

ctx_uniq < apply IH to H6 H4 H5.
```
```Subgoal 2.2:

Variables: L, E, T1, T2, L1, B, L2, T
IH : forall L E T1 T2, ctx L -> member (of E T1) L * ->
member (of E T2) L -> T1 = T2
H4 : member (of (E n1) T2) L2 *
H5 : member (of (E n1) T2) L2
H6 : ctx L2
============================
T2 = T2

ctx_uniq < search.
Proof completed.
```
We need another property about the context before we can prove our generalized theorem. We've shown well-formed contexts cannot have two typing judgments for the same variable, but we still have to show that such contexts can only contain typing judgments for nominal constants. For this we define a notation that a term must be a nominal constant.
```Define name : tm -> prop by
nabla x, name x.
```
Given a variable `X` and an assumption `name X`, `X` must be a nominal constant by the definition of `name`. The structural property about a well-formed context is basically an inspection of its definition, which is stated as follows.
```Theorem ctx_mem : forall L E,
ctx L -> member E L ->  exists N X, E = of X N /\ name X.
```
The proof of this lemma is straightforward so I'll just show it.
```

============================
forall L E, ctx L -> member E L -> (exists N X, E = of X N /\ name X)

ctx_mem < induction on 2.
```
```

IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X)
============================
forall L E, ctx L -> member E L @ -> (exists N X, E = of X N /\ name X)

ctx_mem < intros.
```
```
Variables: L, E
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\
name X)
H1 : ctx L
H2 : member E L @
============================
exists N X, E = of X N /\ name X

ctx_mem < case H2.
```
```Subgoal 1:

Variables: L, E, L1
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\
name X)
H1 : ctx (E :: L1)
============================
exists N X, E = of X N /\ name X

Subgoal 2 is:
exists N X, E = of X N /\ name X

ctx_mem < case H1.
```
```Subgoal 1:

Variables: L, E, L1, L2, T
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\
name X)
H3 : ctx L2
============================
exists N X, of n1 T = of X N /\ name X

Subgoal 2 is:
exists N X, E = of X N /\ name X

ctx_mem < search.
```
```Subgoal 2:

Variables: L, E, L1, B
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\
name X)
H1 : ctx (B :: L1)
H3 : member E L1 *
============================
exists N X, E = of X N /\ name X

ctx_mem < case H1.
```
```Subgoal 2:

Variables: L, E, L1, B, L2, T
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\
name X)
H3 : member (E n1) L2 *
H4 : ctx L2
============================
exists N X, E n1 = of X N /\ name X

ctx_mem < apply IH to H4 H3.
```
```Subgoal 2:

Variables: L, E, L1, B, L2, T, N, X
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\
name X)
H3 : member (of (X n1) N) L2 *
H4 : ctx L2
H5 : name (X n1)
============================
exists N1 X1, of (X n1) N = of X1 N1 /\ name X1

ctx_mem < search.
Proof completed.
```
Notice that at one point we did case analysis on `ctx (E :: L1)` which exposes `E` to be `of n1 T`. Since `n1` is a nominal constant, a `search` completed the subgoal.

Now we can state and prove our generalized theorem.

```Theorem type_uniq_ext : forall L E T1 T2,
ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.
```
The proof of this lemma is by induction on one of the typing judgments. The body of the proof consists of considering the possible ways in which the two typing judgments are derived. Because these typing judgments have non-empty contexts, we will have to consider the possibility that, for example, the typing judgment ```(of E T1)``` comes directly from the context `L`. Thus case analysis on a hypothesis like `{L |- of E T1}` will result in three subgoals.

The entire proof is listed below. We pay special attention to cases where the typing judgment is derived from the context. We will also pause to introduce a convenient feature of the `apply` tactic.

```

============================
forall L E T1 T2, ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2

type_uniq_ext < induction on 2.
```
```

IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
============================
forall L E T1 T2, ctx L -> {L |- of E T1}@ -> {L |- of E T2} -> T1 = T2

type_uniq_ext < intros.
```
```
Variables: L, E, T1, T2
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H2 : {L |- of E T1}@
H3 : {L |- of E T2}
============================
T1 = T2

type_uniq_ext < case H2.
```
In the first case, the goal formula `of E T1` is derived from the program clause for abstraction.
```Subgoal 1:

Variables: L, E, T1, T2, U, R, T
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H3 : {L |- of (abs T R) T2}
H4 : {L, of n1 T |- of (R n1) U}*
============================
arrow T U = T2

Subgoal 2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < case H3.
```
```Subgoal 1.1:

Variables: L, E, T1, T2, U, R, T, U1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L, of n1 T |- of (R n1) U}*
H5 : {L, of n1 T |- of (R n1) U1}
============================
arrow T U = arrow T U1

Subgoal 1.2 is:
arrow T U = T2

Subgoal 2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < apply IH to _ H4 H5.
```
We are now considering the case when `E` is the abstraction `(abs T R)` and the typing judgments are formed using the typing rule for abstractions. Thus the typing context has grown to include a typing assumption for a new nominal constant `n1`. In order to apply our inductive hypothesis to the new typing judgments for `(R n1)`, we must ensure that `(of n1 T :: L)` is a well-formed context, i.e. that it is accepted by the definition of `ctx`. This should be easy since it is clear that neither `T` nor `L` can depends on `n1`.

One option is to use the `assert` tactic to explicitly state `ctx (of n1 T :: L)`. We could then prove this assertion using the `search` tactic. A more convenient option is to use what is called "apply with unknowns." For this we simply put a `_` where we want the system to generate a hypothesis for us. The prover will then guess what needs be proved for the unknown hypothesis and attempt to prove it using the `search` tactic. If this fails, the current subgoal will be delayed and the unknown hypothesis will become the current goal. In our case, `ctx (of n1 T :: L)` will be solved by `search` so there is no extra subgoal generated. We now return you to the rest of the proof.

```Subgoal 1.1:

Variables: L, E, T1, T2, U, R, T, U1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L, of n1 T |- of (R n1) U1}*
H5 : {L, of n1 T |- of (R n1) U1}
============================
arrow T U1 = arrow T U1

Subgoal 1.2 is:
arrow T U = T2

Subgoal 2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < search.
```
```Subgoal 1.2:

Variables: L, E, T1, T2, U, R, T, F
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L, of n1 T |- of (R n1) U}*
H5 : {L, [F] |- of (abs T R) T2}
H6 : member F L
============================
arrow T U = T2

Subgoal 2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < apply ctx_mem to H1 H6.
```
At this point we encounter a judgment of the form ```{L, [F] |- G} ``` for the first time. Such a judgment is called a backchaining judgment, which indicates that the goal formula `G` , which is `of (abs T R) T2` in this case, is proved by backchaining on some formula `F` in the context `L`. The hypothesis `member F L` is introduced to show that `F` is contained in `L`.

If we perform case analysis on `H5`, we will get an error message:

```type_uniq_ext < case H5.
Error: Cannot perform case-analysis on flexible head
```
Case analysis fails because the structure of `F` is unknown. To make progress we apply the lemma `ctx_mem` to reveal `F`, which is of the form `of X N`. Then we perform case analysis on `H5` which backchains the goal `of (abs T R) T2` on the clause `of X N`, as shown below.
```Subgoal 1.2:

Variables: L, E, T1, T2, U, R, T, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L, of n1 T |- of (R n1) U}*
H5 : {L, [of X N] |- of (abs T R) T2}
H6 : member (of X N) L
H7 : name X
============================
arrow T U = T2

Subgoal 2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < case H5.
```
```Subgoal 1.2:

Variables: L, E, T1, T2, U, R, T, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L, of n1 T |- of (R n1) U}*
H6 : member (of (abs T R) T2) L
H7 : name (abs T R)
============================
arrow T U = T2

Subgoal 2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < case H7.
```
As a result of backchaining, `X` is unified with `abs T R`. Case analysis on `H7` completed this subgoal because `abs T R` is not a nominal constant.

The case that `E` is an application is proved in a similar way.

```Subgoal 2:

Variables: L, E, T1, T2, U, N, M
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H3 : {L |- of (app M N) T2}
H4 : {L |- of M (arrow U T1)}*
H5 : {L |- of N U}*
============================
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < case H3.
```
```Subgoal 2.1:

Variables: L, E, T1, T2, U, N, M, U1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L |- of M (arrow U T1)}*
H5 : {L |- of N U}*
H6 : {L |- of M (arrow U1 T2)}
H7 : {L |- of N U1}
============================
T1 = T2

Subgoal 2.2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < apply IH to H1 H4 H6.
```
```Subgoal 2.1:

Variables: L, E, T1, T2, U, N, M, U1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L |- of M (arrow U1 T2)}*
H5 : {L |- of N U1}*
H6 : {L |- of M (arrow U1 T2)}
H7 : {L |- of N U1}
============================
T2 = T2

Subgoal 2.2 is:
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < search.
```
```Subgoal 2.2:

Variables: L, E, T1, T2, U, N, M, F
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L |- of M (arrow U T1)}*
H5 : {L |- of N U}*
H6 : {L, [F] |- of (app M N) T2}
H7 : member F L
============================
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < apply ctx_mem to H1 H7.
```
```Subgoal 2.2:

Variables: L, E, T1, T2, U, N, M, F, N1, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L |- of M (arrow U T1)}*
H5 : {L |- of N U}*
H6 : {L, [of X N1] |- of (app M N) T2}
H7 : member (of X N1) L
H8 : name X
============================
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < case H6.
```
```Subgoal 2.2:

Variables: L, E, T1, T2, U, N, M, F, N1, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L |- of M (arrow U T1)}*
H5 : {L |- of N U}*
H7 : member (of (app M N) T2) L
H8 : name (app M N)
============================
T1 = T2

Subgoal 3 is:
T1 = T2

type_uniq_ext < case H8.
```
The last case is when the goal formula is derived from some clause `F` in the context. As described before, we first apply the lemma `ctx_mem` to reveal the structure of `F`. We then perform case analysis to backchain the goal formula on `F`.
```Subgoal 3:

Variables: L, E, T1, T2, F
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H4 : {L, [F] |- of E T1}*
H5 : member F L
============================
T1 = T2

type_uniq_ext < apply ctx_mem to H1 H5.
```
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H4 : {L, [of X N] |- of E T1}*
H5 : member (of X N) L
H6 : name X
============================
T1 = T2

type_uniq_ext < case H4.
```
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H5 : member (of E T1) L
H6 : name E
============================
T1 = T2

type_uniq_ext < case H6.
```
The case analysis above reveals the fact that `E` is a nominal constant. Eigenvariables are raised over this nominal constant `n1` because of their dependency on `n1`. Now the goal formula `of n1 T2` in `H3` can only be derived from the context because the nominal constant `n1` cannot be an abstraction or an application. The same technique for reasoning about backchaining judgments is used once again for `{L n1 |- of n1 T2}`.
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx (L n1)
H3 : {L n1 |- of n1 T2}
H5 : member (of n1 T1) (L n1)
============================
T1 = T2

type_uniq_ext < case H3.
```
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X, F1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx (L n1)
H5 : member (of n1 T1) (L n1)
H7 : {L n1, [F1 n1] |- of n1 T2}
H8 : member (F1 n1) (L n1)
============================
T1 = T2

type_uniq_ext < apply ctx_mem to H1 H8.
```
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X, F1, N1, X1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx (L n1)
H5 : member (of n1 T1) (L n1)
H7 : {L n1, [of (X1 n1) N1] |- of n1 T2}
H8 : member (of (X1 n1) N1) (L n1)
H9 : name (X1 n1)
============================
T1 = T2

type_uniq_ext < case H7.
```
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X, F1, N1, X1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx (L n1)
H5 : member (of n1 T1) (L n1)
H8 : member (of n1 T2) (L n1)
H9 : name n1
============================
T1 = T2

type_uniq_ext < apply ctx_uniq to H1 H5 H8.
```
At this point we know `of n1 T1` and `of n1 T2` are both in the same context. By applying `ctx_uniq` we prove that `T1` and `T2` are the same.
```Subgoal 3:

Variables: L, E, T1, T2, F, N, X, F1, N1, X1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx (L n1)
H5 : member (of n1 T2) (L n1)
H8 : member (of n1 T2) (L n1)
H9 : name n1
============================
T2 = T2

type_uniq_ext < search.
Proof completed.
```
We can now use this generalized theorem to prove our specific theorem. Watch closely and you'll see another use of apply with unknowns.
```Abella < Theorem type_uniq : forall E T1 T2,
{of E T1} -> {of E T2} -> T1 = T2.

============================
forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2

type_uniq < intros.
```
```
Variables: E, T1, T2
H1 : {of E T1}
H2 : {of E T2}
============================
T1 = T2

type_uniq < apply type_uniq_ext to _ H1 H2.
```
```
Variables: E, T1, T2
H1 : {of E T2}
H2 : {of E T2}
============================
T2 = T2

type_uniq < search.
Proof completed.
```
Congratulations! We've now proved type uniqueness for the simply-typed lambda-calculus. You can look at examples/lambda-calculus/type-uniq/type-uniq.thm for a full development.

You should now have a basic understanding of the most popular tactics in Abella as well as of definitions and lemmas. With this knowledge you are ready to understand any of the examples included with Abella. I suggest looking at the examples listed on the homepage and perhaps those smaller examples listed here. You are also encourage to specify and reason about your own logical system. If so, please let us hear about it: Abella mailing list