Welcome to Abella 2.0.5-dev.
```Abella < Specification "debruijn".

```
```Abella < Theorem member_prune :
forall E L, nabla x, member (E x) L -> (exists F, E = y\F).

```
```
============================
forall E L, nabla x, member (E x) L -> (exists F, E = y\F)

member_prune < induction on 1.
```
```
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
forall E L, nabla x, member (E x) L @ -> (exists F, E = y\F)

member_prune < intros.
```
```
Variables: E L
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
exists F, E = y\F

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

Variables: L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
exists F, z1\L2 = y\F

Subgoal 2 is:
exists F, E = y\F

member_prune < search.
```
```Subgoal 2:

Variables: E L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
exists F, E = y\F

member_prune < apply IH to H2.
```
```Subgoal 2:

Variables: L3 L2 F
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
exists F1, z1\F = y\F1

member_prune < search.
Proof completed.
```
```Abella < Define nat : nat -> prop by
nat z;
nat (s X) := nat X.

```
```Abella < Define le : nat -> nat -> prop by
le X X;
le X (s Y) := le X Y.

```
```Abella < Theorem le_dec :
forall X Y, le (s X) Y -> le X Y.

```
```
============================
forall X Y, le (s X) Y -> le X Y

le_dec < induction on 1.
```
```
IH : forall X Y, le (s X) Y * -> le X Y
============================
forall X Y, le (s X) Y @ -> le X Y

le_dec < intros.
```
```
Variables: X Y
IH : forall X Y, le (s X) Y * -> le X Y
H1 : le (s X) Y @
============================
le X Y

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

Variables: X
IH : forall X Y, le (s X) Y * -> le X Y
============================
le X (s X)

Subgoal 2 is:
le X (s Y1)

le_dec < search.
```
```Subgoal 2:

Variables: X Y1
IH : forall X Y, le (s X) Y * -> le X Y
H2 : le (s X) Y1 *
============================
le X (s Y1)

le_dec < apply IH to H2.
```
```Subgoal 2:

Variables: X Y1
IH : forall X Y, le (s X) Y * -> le X Y
H2 : le (s X) Y1 *
H3 : le X Y1
============================
le X (s Y1)

le_dec < search.
Proof completed.
```
```Abella < Theorem le_absurd :
forall X, nat X -> le (s X) X -> false.

```
```
============================
forall X, nat X -> le (s X) X -> false

le_absurd < induction on 1.
```
```
IH : forall X, nat X * -> le (s X) X -> false
============================
forall X, nat X @ -> le (s X) X -> false

le_absurd < intros.
```
```
Variables: X
IH : forall X, nat X * -> le (s X) X -> false
H1 : nat X @
H2 : le (s X) X
============================
false

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

IH : forall X, nat X * -> le (s X) X -> false
H2 : le (s z) z
============================
false

Subgoal 2 is:
false

le_absurd < case H2.
```
```Subgoal 2:

Variables: X1
IH : forall X, nat X * -> le (s X) X -> false
H2 : le (s (s X1)) (s X1)
H3 : nat X1 *
============================
false

le_absurd < case H2.
```
```Subgoal 2:

Variables: X1
IH : forall X, nat X * -> le (s X) X -> false
H3 : nat X1 *
H4 : le (s (s X1)) X1
============================
false

le_absurd < apply le_dec to H4.
```
```Subgoal 2:

Variables: X1
IH : forall X, nat X * -> le (s X) X -> false
H3 : nat X1 *
H4 : le (s (s X1)) X1
H5 : le (s X1) X1
============================
false

le_absurd < apply IH to H3 H5.
Proof completed.
```
```Abella < Theorem add_le :
forall A B C, {add A B C} -> le B C.

```
```
============================
forall A B C, {add A B C} -> le B C

```
```
IH : forall A B C, {add A B C}* -> le B C
============================
forall A B C, {add A B C}@ -> le B C

```
```
Variables: A B C
IH : forall A B C, {add A B C}* -> le B C
H1 : {add A B C}@
============================
le B C

```
```Subgoal 1:

Variables: C
IH : forall A B C, {add A B C}* -> le B C
============================
le C C

Subgoal 2 is:
le B (s C1)

```
```Subgoal 2:

Variables: B C1 A1
IH : forall A B C, {add A B C}* -> le B C
H2 : {add A1 B C1}*
============================
le B (s C1)

add_le < apply IH to H2.
```
```Subgoal 2:

Variables: B C1 A1
IH : forall A B C, {add A B C}* -> le B C
H2 : {add A1 B C1}*
H3 : le B C1
============================
le B (s C1)

Proof completed.
```
```Abella < Theorem add_absurd :
forall A C, nat C -> {add A (s C) C} -> false.

```
```
============================
forall A C, nat C -> {add A (s C) C} -> false

```
```
Variables: A C
H1 : nat C
H2 : {add A (s C) C}
============================
false

```
```
Variables: A C
H1 : nat C
H2 : {add A (s C) C}
H3 : le (s C) C
============================
false

add_absurd < apply le_absurd to H1 H3.
Proof completed.
```
```Abella < Theorem add_zero :
forall A C, nat C -> {add A C C} -> A = z.

```
```
============================
forall A C, nat C -> {add A C C} -> A = z

```
```
Variables: A C
H1 : nat C
H2 : {add A C C}
============================
A = z

```
```Subgoal 1:

Variables: C
H1 : nat C
============================
z = z

Subgoal 2 is:
s A1 = z

```
```Subgoal 2:

Variables: C1 A1
H1 : nat (s C1)
H3 : {add A1 (s C1) C1}
============================
s A1 = z

```
```Subgoal 2:

Variables: C1 A1
H3 : {add A1 (s C1) C1}
H4 : nat C1
============================
s A1 = z

Proof completed.
```
```Abella < Theorem add_det1 :
forall A1 A2 B C, nat C -> {add A1 B C} -> {add A2 B C} -> A1 = A2.

```
```
============================
forall A1 A2 B C, nat C -> {add A1 B C} -> {add A2 B C} -> A1 = A2

```
```
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
============================
forall A1 A2 B C, nat C -> {add A1 B C}@ -> {add A2 B C} -> A1 = A2

```
```
Variables: A1 A2 B C
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H1 : nat C
H2 : {add A1 B C}@
H3 : {add A2 B C}
============================
A1 = A2

```
```Subgoal 1:

Variables: A2 C
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H1 : nat C
H3 : {add A2 C C}
============================
z = A2

Subgoal 2 is:
s A = A2

```
```Subgoal 1:

Variables: C
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H1 : nat C
H3 : {add z C C}
============================
z = z

Subgoal 2 is:
s A = A2

```
```Subgoal 2:

Variables: A2 B C1 A
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H1 : nat (s C1)
H3 : {add A2 B (s C1)}
H4 : {add A B C1}*
============================
s A = A2

```
```Subgoal 2.1:

Variables: C1 A
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H1 : nat (s C1)
H4 : {add A (s C1) C1}*
============================
s A = z

Subgoal 2.2 is:
s A = s A3

```
```Subgoal 2.1:

Variables: C1 A
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H4 : {add A (s C1) C1}*
H5 : nat C1
============================
s A = z

Subgoal 2.2 is:
s A = s A3

```
```Subgoal 2.2:

Variables: B C1 A A3
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H1 : nat (s C1)
H4 : {add A B C1}*
H5 : {add A3 B C1}
============================
s A = s A3

```
```Subgoal 2.2:

Variables: B C1 A A3
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H4 : {add A B C1}*
H5 : {add A3 B C1}
H6 : nat C1
============================
s A = s A3

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

Variables: B C1 A3
IH : forall A1 A2 B C, nat C -> {add A1 B C}* -> {add A2 B C} -> A1 = A2
H4 : {add A3 B C1}*
H5 : {add A3 B C1}
H6 : nat C1
============================
s A3 = s A3

Proof completed.
```
```Abella < Theorem add_det2 :
forall A B1 B2 C, {add A B1 C} -> {add A B2 C} -> B1 = B2.

```
```
============================
forall A B1 B2 C, {add A B1 C} -> {add A B2 C} -> B1 = B2

```
```
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
============================
forall A B1 B2 C, {add A B1 C}@ -> {add A B2 C} -> B1 = B2

```
```
Variables: A B1 B2 C
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
H1 : {add A B1 C}@
H2 : {add A B2 C}
============================
B1 = B2

```
```Subgoal 1:

Variables: B2 C
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
H2 : {add z B2 C}
============================
C = B2

Subgoal 2 is:
B1 = B2

```
```Subgoal 1:

Variables: C
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
============================
C = C

Subgoal 2 is:
B1 = B2

```
```Subgoal 2:

Variables: B1 B2 C1 A1
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
H2 : {add (s A1) B2 (s C1)}
H3 : {add A1 B1 C1}*
============================
B1 = B2

```
```Subgoal 2:

Variables: B1 B2 C1 A1
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
H3 : {add A1 B1 C1}*
H4 : {add A1 B2 C1}
============================
B1 = B2

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

Variables: B2 C1 A1
IH : forall A B1 B2 C, {add A B1 C}* -> {add A B2 C} -> B1 = B2
H3 : {add A1 B2 C1}*
H4 : {add A1 B2 C1}
============================
B2 = B2

Proof completed.
```
```Abella < Define ctx : olist -> nat -> prop by
ctx nil z;
nabla x, ctx (depth x H :: L) (s H) := ctx L H.

```
```Abella < Define name : hterm -> prop by
nabla x, name x.

```
```Abella < Theorem ctx_nat :
forall L H, ctx L H -> nat H.

```
```
============================
forall L H, ctx L H -> nat H

ctx_nat < induction on 1.
```
```
IH : forall L H, ctx L H * -> nat H
============================
forall L H, ctx L H @ -> nat H

ctx_nat < intros.
```
```
Variables: L H
IH : forall L H, ctx L H * -> nat H
H1 : ctx L H @
============================
nat H

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

IH : forall L H, ctx L H * -> nat H
============================
nat z

Subgoal 2 is:
nat (s H1)

ctx_nat < search.
```
```Subgoal 2:

Variables: H1 L1
IH : forall L H, ctx L H * -> nat H
H2 : ctx L1 H1 *
============================
nat (s H1)

ctx_nat < apply IH to H2.
```
```Subgoal 2:

Variables: H1 L1
IH : forall L H, ctx L H * -> nat H
H2 : ctx L1 H1 *
H3 : nat H1
============================
nat (s H1)

ctx_nat < search.
Proof completed.
```
```Abella < Theorem ctx_world :
forall E L H, ctx L H -> member E L ->
(exists X HX, E = depth X HX /\ name X).

```
```
============================
forall E L H, ctx L H -> member E L ->
(exists X HX, E = depth X HX /\ name X)

ctx_world < induction on 1.
```
```
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
============================
forall E L H, ctx L H @ -> member E L ->
(exists X HX, E = depth X HX /\ name X)

ctx_world < intros.
```
```
Variables: E L H
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H1 : ctx L H @
H2 : member E L
============================
exists X HX, E = depth X HX /\ name X

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

Variables: E
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H2 : member E nil
============================
exists X HX, E = depth X HX /\ name X

Subgoal 2 is:
exists X HX, E n1 = depth X HX /\ name X

ctx_world < case H2.
```
```Subgoal 2:

Variables: E H1 L1
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H2 : member (E n1) (depth n1 H1 :: L1)
H3 : ctx L1 H1 *
============================
exists X HX, E n1 = depth X HX /\ name X

ctx_world < case H2.
```
```Subgoal 2.1:

Variables: H1 L1
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H3 : ctx L1 H1 *
============================
exists X HX, depth n1 H1 = depth X HX /\ name X

Subgoal 2.2 is:
exists X HX, E n1 = depth X HX /\ name X

ctx_world < search.
```
```Subgoal 2.2:

Variables: E H1 L1
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H3 : ctx L1 H1 *
H4 : member (E n1) L1
============================
exists X HX, E n1 = depth X HX /\ name X

ctx_world < apply member_prune to H4.
```
```Subgoal 2.2:

Variables: H1 L1 F
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H3 : ctx L1 H1 *
H4 : member F L1
============================
exists X HX, F = depth X HX /\ name X

ctx_world < apply IH to H3 H4.
```
```Subgoal 2.2:

Variables: H1 L1 X HX
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = depth X HX /\ name X)
H3 : ctx L1 H1 *
H4 : member (depth X HX) L1
H5 : name X
============================
exists X1 HX1, depth X HX = depth X1 HX1 /\ name X1

ctx_world < search.
Proof completed.
```
```Abella < Theorem depth_name :
forall L H X HX, ctx L H -> {L |- depth X HX} -> name X.

```
```
============================
forall L H X HX, ctx L H -> {L |- depth X HX} -> name X

depth_name < intros.
```
```
Variables: L H X HX
H1 : ctx L H
H2 : {L |- depth X HX}
============================
name X

depth_name < case H2.
```
```
Variables: L H X HX F
H1 : ctx L H
H3 : {L, [F] |- depth X HX}
H4 : member F L
============================
name X

depth_name < apply ctx_world to H1 H4.
```
```
Variables: L H X HX X1 HX1
H1 : ctx L H
H3 : {L, [depth X1 HX1] |- depth X HX}
H4 : member (depth X1 HX1) L
H5 : name X1
============================
name X

depth_name < case H3.
```
```
Variables: L H X HX
H1 : ctx L H
H4 : member (depth X HX) L
H5 : name X
============================
name X

depth_name < search.
Proof completed.
```
```Abella < Theorem member_depth_det2 :
forall L H X H1 H2, ctx L H -> member (depth X H1) L ->
member (depth X H2) L -> H1 =
H2.

```
```
============================
forall L H X H1 H2, ctx L H -> member (depth X H1) L ->
member (depth X H2) L -> H1 =
H2

member_depth_det2 < induction on 2.
```
```
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
============================
forall L H X H1 H2, ctx L H -> member (depth X H1) L @ ->
member (depth X H2) L -> H1 =
H2

member_depth_det2 < intros.
```
```
Variables: L H X H1 H2
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx L H
H2 : member (depth X H1) L @
H3 : member (depth X H2) L
============================
H1 = H2

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

Variables: H X H1 H2 L1
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx (depth X H1 :: L1) H
H3 : member (depth X H2) (depth X H1 :: L1)
============================
H1 = H2

Subgoal 2 is:
H1 = H2

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

Variables: H X H1 L1
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx (depth X H1 :: L1) H
============================
H1 = H1

Subgoal 1.2 is:
H1 = H2

Subgoal 2 is:
H1 = H2

member_depth_det2 < search.
```
```Subgoal 1.2:

Variables: H X H1 H2 L1
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx (depth X H1 :: L1) H
H4 : member (depth X H2) L1
============================
H1 = H2

Subgoal 2 is:
H1 = H2

member_depth_det2 < case H1.
```
```Subgoal 1.2:

Variables: H2 H3 L2
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H4 : member (depth n1 (H2 n1)) L2
H5 : ctx L2 H3
============================
H3 = H2 n1

Subgoal 2 is:
H1 = H2

member_depth_det2 < apply member_prune to H4.
```
```Subgoal 2:

Variables: H X H1 H2 L1 B
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx (B :: L1) H
H3 : member (depth X H2) (B :: L1)
H4 : member (depth X H1) L1 *
============================
H1 = H2

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

Variables: H X H1 H2 L1
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx (depth X H2 :: L1) H
H4 : member (depth X H1) L1 *
============================
H1 = H2

Subgoal 2.2 is:
H1 = H2

member_depth_det2 < case H1.
```
```Subgoal 2.1:

Variables: H1 H3 L2
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H4 : member (depth n1 (H1 n1)) L2 *
H5 : ctx L2 H3
============================
H1 n1 = H3

Subgoal 2.2 is:
H1 = H2

member_depth_det2 < apply member_prune to H4.
```
```Subgoal 2.2:

Variables: H X H1 H2 L1 B
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H1 : ctx (B :: L1) H
H4 : member (depth X H1) L1 *
H5 : member (depth X H2) L1
============================
H1 = H2

member_depth_det2 < case H1.
```
```Subgoal 2.2:

Variables: X H1 H2 H3 L2
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H4 : member (depth (X n1) (H1 n1)) L2 *
H5 : member (depth (X n1) (H2 n1)) L2
H6 : ctx L2 H3
============================
H1 n1 = H2 n1

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

Variables: X H2 H3 L2
IH : forall L H X H1 H2, ctx L H -> member (depth X H1) L * ->
member (depth X H2) L -> H1 =
H2
H4 : member (depth (X n1) (H2 n1)) L2 *
H5 : member (depth (X n1) (H2 n1)) L2
H6 : ctx L2 H3
============================
H2 n1 = H2 n1

member_depth_det2 < search.
Proof completed.
```
```Abella < Theorem depth_det2 :
forall L H X H1 H2, ctx L H -> {L |- depth X H1} -> {L |- depth X H2} -> H1 =
H2.

```
```
============================
forall L H X H1 H2, ctx L H -> {L |- depth X H1} -> {L |- depth X H2} ->
H1 =
H2

depth_det2 < intros.
```
```
Variables: L H X H1 H2
H1 : ctx L H
H2 : {L |- depth X H1}
H3 : {L |- depth X H2}
============================
H1 = H2

depth_det2 < case H2.
```
```
Variables: L H X H1 H2 F
H1 : ctx L H
H3 : {L |- depth X H2}
H4 : {L, [F] |- depth X H1}
H5 : member F L
============================
H1 = H2

depth_det2 < apply ctx_world to H1 H5.
```
```
Variables: L H X H1 H2 X1 HX
H1 : ctx L H
H3 : {L |- depth X H2}
H4 : {L, [depth X1 HX] |- depth X H1}
H5 : member (depth X1 HX) L
H6 : name X1
============================
H1 = H2

depth_det2 < case H4.
```
```
Variables: L H X H1 H2
H1 : ctx L H
H3 : {L |- depth X H2}
H5 : member (depth X H1) L
H6 : name X
============================
H1 = H2

depth_det2 < case H3.
```
```
Variables: L H X H1 H2 F1
H1 : ctx L H
H5 : member (depth X H1) L
H6 : name X
H7 : {L, [F1] |- depth X H2}
H8 : member F1 L
============================
H1 = H2

depth_det2 < apply ctx_world to H1 H8.
```
```
Variables: L H X H1 H2 X2 HX1
H1 : ctx L H
H5 : member (depth X H1) L
H6 : name X
H7 : {L, [depth X2 HX1] |- depth X H2}
H8 : member (depth X2 HX1) L
H9 : name X2
============================
H1 = H2

depth_det2 < case H7.
```
```
Variables: L H X H1 H2
H1 : ctx L H
H5 : member (depth X H1) L
H6 : name X
H8 : member (depth X H2) L
H9 : name X
============================
H1 = H2

depth_det2 < case H6.
```
```
Variables: L H H1 H2
H1 : ctx (L n1) (H n1)
H5 : member (depth n1 (H1 n1)) (L n1)
H8 : member (depth n1 (H2 n1)) (L n1)
H9 : name n1
============================
H1 n1 = H2 n1

depth_det2 < apply member_depth_det2 to H1 H5 H8.
```
```
Variables: L H H2
H1 : ctx (L n1) (H n1)
H5 : member (depth n1 (H2 n1)) (L n1)
H8 : member (depth n1 (H2 n1)) (L n1)
H9 : name n1
============================
H2 n1 = H2 n1

depth_det2 < search.
Proof completed.
```
```Abella < Theorem ctx_member_absurd :
forall X H1 H2 L, ctx L H1 -> member (depth X H2) L -> le H1 H2 -> false.

```
```
============================
forall X H1 H2 L, ctx L H1 -> member (depth X H2) L -> le H1 H2 -> false

ctx_member_absurd < induction on 2.
```
```
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
============================
forall X H1 H2 L, ctx L H1 -> member (depth X H2) L @ -> le H1 H2 -> false

ctx_member_absurd < intros.
```
```
Variables: X H1 H2 L
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H1 : ctx L H1
H2 : member (depth X H2) L @
H3 : le H1 H2
============================
false

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

Variables: X H1 H2 L1
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H1 : ctx (depth X H2 :: L1) H1
H3 : le H1 H2
============================
false

Subgoal 2 is:
false

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

Variables: H L2
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H3 : le (s H) H
H4 : ctx L2 H
============================
false

Subgoal 2 is:
false

ctx_member_absurd < apply ctx_nat to H4.
```
```Subgoal 1:

Variables: H L2
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H3 : le (s H) H
H4 : ctx L2 H
H5 : nat H
============================
false

Subgoal 2 is:
false

ctx_member_absurd < apply le_absurd to H5 H3.
```
```Subgoal 2:

Variables: X H1 H2 L1 B
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H1 : ctx (B :: L1) H1
H3 : le H1 H2
H4 : member (depth X H2) L1 *
============================
false

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

Variables: X H2 H L2
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H3 : le (s H) (H2 n1)
H4 : member (depth (X n1) (H2 n1)) L2 *
H5 : ctx L2 H
============================
false

ctx_member_absurd < apply member_prune to H4.
```
```Subgoal 2:

Variables: H L2 F2 F1
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H3 : le (s H) F2
H4 : member (depth F1 F2) L2 *
H5 : ctx L2 H
============================
false

ctx_member_absurd < apply le_dec to H3.
```
```Subgoal 2:

Variables: H L2 F2 F1
IH : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L * -> le H1 H2 ->
false
H3 : le (s H) F2
H4 : member (depth F1 F2) L2 *
H5 : ctx L2 H
H6 : le H F2
============================
false

ctx_member_absurd < apply IH to H5 H4 H6.
Proof completed.
```
```Abella < Theorem member_depth_det1 :
forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L ->
member (depth X2 HX) L -> X1 =
X2.

```
```
============================
forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L ->
member (depth X2 HX) L -> X1 =
X2

member_depth_det1 < induction on 2.
```
```
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
============================
forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L @ ->
member (depth X2 HX) L -> X1 =
X2

member_depth_det1 < intros.
```
```
Variables: L H X1 X2 HX
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx L H
H2 : member (depth X1 HX) L @
H3 : member (depth X2 HX) L
============================
X1 = X2

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

Variables: H X1 X2 HX L1
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx (depth X1 HX :: L1) H
H3 : member (depth X2 HX) (depth X1 HX :: L1)
============================
X1 = X2

Subgoal 2 is:
X1 = X2

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

Variables: H X1 HX L1
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx (depth X1 HX :: L1) H
============================
X1 = X1

Subgoal 1.2 is:
X1 = X2

Subgoal 2 is:
X1 = X2

member_depth_det1 < search.
```
```Subgoal 1.2:

Variables: H X1 X2 HX L1
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx (depth X1 HX :: L1) H
H4 : member (depth X2 HX) L1
============================
X1 = X2

Subgoal 2 is:
X1 = X2

member_depth_det1 < case H1.
```
```Subgoal 1.2:

Variables: X2 H1 L2
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H4 : member (depth (X2 n1) H1) L2
H5 : ctx L2 H1
============================
n1 = X2 n1

Subgoal 2 is:
X1 = X2

member_depth_det1 < apply ctx_member_absurd to H5 H4 _.
```
```Subgoal 2:

Variables: H X1 X2 HX L1 B
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx (B :: L1) H
H3 : member (depth X2 HX) (B :: L1)
H4 : member (depth X1 HX) L1 *
============================
X1 = X2

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

Variables: H X1 X2 HX L1
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx (depth X2 HX :: L1) H
H4 : member (depth X1 HX) L1 *
============================
X1 = X2

Subgoal 2.2 is:
X1 = X2

member_depth_det1 < case H1.
```
```Subgoal 2.1:

Variables: X1 H1 L2
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H4 : member (depth (X1 n1) H1) L2 *
H5 : ctx L2 H1
============================
X1 n1 = n1

Subgoal 2.2 is:
X1 = X2

member_depth_det1 < apply ctx_member_absurd to H5 H4 _.
```
```Subgoal 2.2:

Variables: H X1 X2 HX L1 B
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H1 : ctx (B :: L1) H
H4 : member (depth X1 HX) L1 *
H5 : member (depth X2 HX) L1
============================
X1 = X2

member_depth_det1 < case H1.
```
```Subgoal 2.2:

Variables: X1 X2 HX H1 L2
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H4 : member (depth (X1 n1) (HX n1)) L2 *
H5 : member (depth (X2 n1) (HX n1)) L2
H6 : ctx L2 H1
============================
X1 n1 = X2 n1

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

Variables: X2 HX H1 L2
IH : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L * ->
member (depth X2 HX) L -> X1 =
X2
H4 : member (depth (X2 n1) (HX n1)) L2 *
H5 : member (depth (X2 n1) (HX n1)) L2
H6 : ctx L2 H1
============================
X2 n1 = X2 n1

member_depth_det1 < search.
Proof completed.
```
```Abella < Theorem depth_det1 :
forall L H X1 X2 HX, ctx L H -> {L |- depth X1 HX} -> {L |- depth X2 HX} ->
X1 =
X2.

```
```
============================
forall L H X1 X2 HX, ctx L H -> {L |- depth X1 HX} -> {L |- depth X2 HX} ->
X1 =
X2

depth_det1 < intros.
```
```
Variables: L H X1 X2 HX
H1 : ctx L H
H2 : {L |- depth X1 HX}
H3 : {L |- depth X2 HX}
============================
X1 = X2

depth_det1 < case H2.
```
```
Variables: L H X1 X2 HX F
H1 : ctx L H
H3 : {L |- depth X2 HX}
H4 : {L, [F] |- depth X1 HX}
H5 : member F L
============================
X1 = X2

depth_det1 < case H3.
```
```
Variables: L H X1 X2 HX F F1
H1 : ctx L H
H4 : {L, [F] |- depth X1 HX}
H5 : member F L
H6 : {L, [F1] |- depth X2 HX}
H7 : member F1 L
============================
X1 = X2

depth_det1 < apply ctx_world to H1 H5.
```
```
Variables: L H X1 X2 HX F1 X HX1
H1 : ctx L H
H4 : {L, [depth X HX1] |- depth X1 HX}
H5 : member (depth X HX1) L
H6 : {L, [F1] |- depth X2 HX}
H7 : member F1 L
H8 : name X
============================
X1 = X2

depth_det1 < case H4.
```
```
Variables: L H X1 X2 HX F1
H1 : ctx L H
H5 : member (depth X1 HX) L
H6 : {L, [F1] |- depth X2 HX}
H7 : member F1 L
H8 : name X1
============================
X1 = X2

depth_det1 < apply ctx_world to H1 H7.
```
```
Variables: L H X1 X2 HX X3 HX2
H1 : ctx L H
H5 : member (depth X1 HX) L
H6 : {L, [depth X3 HX2] |- depth X2 HX}
H7 : member (depth X3 HX2) L
H8 : name X1
H9 : name X3
============================
X1 = X2

depth_det1 < case H6.
```
```
Variables: L H X1 X2 HX
H1 : ctx L H
H5 : member (depth X1 HX) L
H7 : member (depth X2 HX) L
H8 : name X1
H9 : name X2
============================
X1 = X2

depth_det1 < case H8.
```
```
Variables: L H X2 HX
H1 : ctx (L n1) (H n1)
H5 : member (depth n1 (HX n1)) (L n1)
H7 : member (depth (X2 n1) (HX n1)) (L n1)
H9 : name (X2 n1)
============================
n1 = X2 n1

depth_det1 < apply member_depth_det1 to H1 H5 H7.
```
```
Variables: L H HX
H1 : ctx (L n1) (H n1)
H5 : member (depth n1 (HX n1)) (L n1)
H7 : member (depth n1 (HX n1)) (L n1)
H9 : name n1
============================
n1 = n1

depth_det1 < search.
Proof completed.
```
```Abella < Theorem add_ignores_ctx :
forall L H A B C, ctx L H -> {L |- add A B C} -> {add A B C}.

```
```
============================
forall L H A B C, ctx L H -> {L |- add A B C} -> {add A B C}

```
```
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
============================
forall L H A B C, ctx L H -> {L |- add A B C}@ -> {add A B C}

```
```
Variables: L H A B C
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
H1 : ctx L H
H2 : {L |- add A B C}@
============================

```
```Subgoal 1:

Variables: L H C
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
H1 : ctx L H
============================

Subgoal 2 is:
{add (s A1) B (s C1)}

Subgoal 3 is:

```
```Subgoal 2:

Variables: L H B C1 A1
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
H1 : ctx L H
H3 : {L |- add A1 B C1}*
============================
{add (s A1) B (s C1)}

Subgoal 3 is:

add_ignores_ctx < apply IH to H1 H3.
```
```Subgoal 2:

Variables: L H B C1 A1
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
H1 : ctx L H
H3 : {L |- add A1 B C1}*
H4 : {add A1 B C1}
============================
{add (s A1) B (s C1)}

Subgoal 3 is:

```
```Subgoal 3:

Variables: L H A B C F
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
H1 : ctx L H
H3 : {L, [F] |- add A B C}*
H4 : member F L
============================

add_ignores_ctx < apply ctx_world to H1 H4.
```
```Subgoal 3:

Variables: L H A B C X HX
IH : forall L H A B C, ctx L H -> {L |- add A B C}* -> {add A B C}
H1 : ctx L H
H3 : {L, [depth X HX] |- add A B C}*
H4 : member (depth X HX) L
H5 : name X
============================

Proof completed.
```
```Abella < Theorem ho2db_det3 :
forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1} -> {L |- ho2db M H D2} ->
D1 =
D2.

```
```
============================
forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1} -> {L |- ho2db M H D2} ->
D1 =
D2

ho2db_det3 < induction on 2.
```
```
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
============================
forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}@ ->
{L |- ho2db M H D2} -> D1 =
D2

ho2db_det3 < intros.
```
```
Variables: L M D1 D2 H
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H2 : {L |- ho2db M H D1}@
H3 : {L |- ho2db M H D2}
============================
D1 = D2

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

Variables: L D2 H DN N DM M1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H3 : {L |- ho2db (app M1 N) H D2}
H4 : {L |- ho2db M1 H DM}*
H5 : {L |- ho2db N H DN}*
============================
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

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

Variables: L H DN N DM M1 DN1 DM1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L |- ho2db M1 H DM1}
H7 : {L |- ho2db N H DN1}
============================
dapp DM DN = dapp DM1 DN1

Subgoal 1.2 is:
dapp DM DN = dvar DX

Subgoal 1.3 is:
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply IH to H1 H4 H6.
```
```Subgoal 1.1:

Variables: L H DN N M1 DN1 DM1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM1}*
H5 : {L |- ho2db N H DN}*
H6 : {L |- ho2db M1 H DM1}
H7 : {L |- ho2db N H DN1}
============================
dapp DM1 DN = dapp DM1 DN1

Subgoal 1.2 is:
dapp DM DN = dvar DX

Subgoal 1.3 is:
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply IH to H1 H5 H7.
```
```Subgoal 1.1:

Variables: L H N M1 DN1 DM1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM1}*
H5 : {L |- ho2db N H DN1}*
H6 : {L |- ho2db M1 H DM1}
H7 : {L |- ho2db N H DN1}
============================
dapp DM1 DN1 = dapp DM1 DN1

Subgoal 1.2 is:
dapp DM DN = dvar DX

Subgoal 1.3 is:
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < search.
```
```Subgoal 1.2:

Variables: L H DN N DM M1 DX HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L |- depth (app M1 N) HX}
H7 : {L |- add HX DX H}
============================
dapp DM DN = dvar DX

Subgoal 1.3 is:
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply depth_name to H1 H6.
```
```Subgoal 1.2:

Variables: L H DN N DM M1 DX HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L |- depth (app M1 N) HX}
H7 : {L |- add HX DX H}
H8 : name (app M1 N)
============================
dapp DM DN = dvar DX

Subgoal 1.3 is:
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H8.
```
```Subgoal 1.3:

Variables: L D2 H DN N DM M1 F
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L, [F] |- ho2db (app M1 N) H D2}
H7 : member F L
============================
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply ctx_world to H1 H7.
```
```Subgoal 1.3:

Variables: L D2 H DN N DM M1 X HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- ho2db M1 H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L, [depth X HX] |- ho2db (app M1 N) H D2}
H7 : member (depth X HX) L
H8 : name X
============================
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H6.
```
```Subgoal 2:

Variables: L D2 H DR R
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H3 : {L |- ho2db (lam R) H D2}
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
============================
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

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

Variables: L H DR R DR1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, depth n1 H |- ho2db (R n1) (s H) DR1}
============================
dlam DR = dlam DR1

Subgoal 2.2 is:
dlam DR = dvar DX

Subgoal 2.3 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply ctx_nat to H1.
```
```Subgoal 2.1:

Variables: L H DR R DR1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, depth n1 H |- ho2db (R n1) (s H) DR1}
H6 : nat H
============================
dlam DR = dlam DR1

Subgoal 2.2 is:
dlam DR = dvar DX

Subgoal 2.3 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply IH to _ H4 H5.
```
```Subgoal 2.1:

Variables: L H R DR1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR1}*
H5 : {L, depth n1 H |- ho2db (R n1) (s H) DR1}
H6 : nat H
============================
dlam DR1 = dlam DR1

Subgoal 2.2 is:
dlam DR = dvar DX

Subgoal 2.3 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < search.
```
```Subgoal 2.2:

Variables: L H DR R DX HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L |- depth (lam R) HX}
H6 : {L |- add HX DX H}
============================
dlam DR = dvar DX

Subgoal 2.3 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply depth_name to H1 H5.
```
```Subgoal 2.2:

Variables: L H DR R DX HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L |- depth (lam R) HX}
H6 : {L |- add HX DX H}
H7 : name (lam R)
============================
dlam DR = dvar DX

Subgoal 2.3 is:
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H7.
```
```Subgoal 2.3:

Variables: L D2 H DR R F
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, [F] |- ho2db (lam R) H D2}
H6 : member F L
============================
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply ctx_world to H1 H6.
```
```Subgoal 2.3:

Variables: L D2 H DR R X HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, [depth X HX] |- ho2db (lam R) H D2}
H6 : member (depth X HX) L
H7 : name X
============================
dlam DR = D2

Subgoal 3 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H5.
```
```Subgoal 3:

Variables: L M D2 H DX HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H3 : {L |- ho2db M H D2}
H4 : {L |- depth M HX}*
H5 : {L |- add HX DX H}*
============================
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H3.
```
```Subgoal 3.1:

Variables: L H DX HX DN N DM M1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth (app M1 N) HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- ho2db M1 H DM}
H7 : {L |- ho2db N H DN}
============================
dvar DX = dapp DM DN

Subgoal 3.2 is:
dvar DX = dlam DR

Subgoal 3.3 is:
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply depth_name to H1 H4.
```
```Subgoal 3.1:

Variables: L H DX HX DN N DM M1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth (app M1 N) HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- ho2db M1 H DM}
H7 : {L |- ho2db N H DN}
H8 : name (app M1 N)
============================
dvar DX = dapp DM DN

Subgoal 3.2 is:
dvar DX = dlam DR

Subgoal 3.3 is:
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H8.
```
```Subgoal 3.2:

Variables: L H DX HX DR R
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth (lam R) HX}*
H5 : {L |- add HX DX H}*
H6 : {L, depth n1 H |- ho2db (R n1) (s H) DR}
============================
dvar DX = dlam DR

Subgoal 3.3 is:
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply depth_name to H1 H4.
```
```Subgoal 3.2:

Variables: L H DX HX DR R
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth (lam R) HX}*
H5 : {L |- add HX DX H}*
H6 : {L, depth n1 H |- ho2db (R n1) (s H) DR}
H7 : name (lam R)
============================
dvar DX = dlam DR

Subgoal 3.3 is:
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H7.
```
```Subgoal 3.3:

Variables: L M H DX HX DX1 HX1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- depth M HX1}
H7 : {L |- add HX1 DX1 H}
============================
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply depth_det2 to H1 H4 H6.
```
```Subgoal 3.3:

Variables: L M H DX DX1 HX1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX1}*
H5 : {L |- add HX1 DX H}*
H6 : {L |- depth M HX1}
H7 : {L |- add HX1 DX1 H}
============================
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply add_ignores_ctx to H1 H5.
```
```Subgoal 3.3:

Variables: L M H DX DX1 HX1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX1}*
H5 : {L |- add HX1 DX H}*
H6 : {L |- depth M HX1}
H7 : {L |- add HX1 DX1 H}
H8 : {add HX1 DX H}
============================
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply add_ignores_ctx to H1 H7.
```
```Subgoal 3.3:

Variables: L M H DX DX1 HX1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX1}*
H5 : {L |- add HX1 DX H}*
H6 : {L |- depth M HX1}
H7 : {L |- add HX1 DX1 H}
H8 : {add HX1 DX H}
H9 : {add HX1 DX1 H}
============================
dvar DX = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply add_det2 to H8 H9.
```
```Subgoal 3.3:

Variables: L M H DX1 HX1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX1}*
H5 : {L |- add HX1 DX1 H}*
H6 : {L |- depth M HX1}
H7 : {L |- add HX1 DX1 H}
H8 : {add HX1 DX1 H}
H9 : {add HX1 DX1 H}
============================
dvar DX1 = dvar DX1

Subgoal 3.4 is:
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < search.
```
```Subgoal 3.4:

Variables: L M D2 H DX HX F
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX}*
H5 : {L |- add HX DX H}*
H6 : {L, [F] |- ho2db M H D2}
H7 : member F L
============================
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < apply ctx_world to H1 H7.
```
```Subgoal 3.4:

Variables: L M D2 H DX HX X HX1
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H4 : {L |- depth M HX}*
H5 : {L |- add HX DX H}*
H6 : {L, [depth X HX1] |- ho2db M H D2}
H7 : member (depth X HX1) L
H8 : name X
============================
dvar DX = D2

Subgoal 4 is:
D1 = D2

ho2db_det3 < case H6.
```
```Subgoal 4:

Variables: L M D1 D2 H F
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H3 : {L |- ho2db M H D2}
H4 : {L, [F] |- ho2db M H D1}*
H5 : member F L
============================
D1 = D2

ho2db_det3 < apply ctx_world to H1 H5.
```
```Subgoal 4:

Variables: L M D1 D2 H X HX
IH : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1}* ->
{L |- ho2db M H D2} -> D1 =
D2
H1 : ctx L H
H3 : {L |- ho2db M H D2}
H4 : {L, [depth X HX] |- ho2db M H D1}*
H5 : member (depth X HX) L
H6 : name X
============================
D1 = D2

ho2db_det3 < case H4.
Proof completed.
```
```Abella < Theorem ho2db_det3_simple :
forall M D1 D2, {ho2db M z D1} -> {ho2db M z D2} -> D1 = D2.

```
```
============================
forall M D1 D2, {ho2db M z D1} -> {ho2db M z D2} -> D1 = D2

ho2db_det3_simple < intros.
```
```
Variables: M D1 D2
H1 : {ho2db M z D1}
H2 : {ho2db M z D2}
============================
D1 = D2

ho2db_det3_simple < apply ho2db_det3 to _ H1 H2.
```
```
Variables: M D2
H1 : {ho2db M z D2}
H2 : {ho2db M z D2}
============================
D2 = D2

ho2db_det3_simple < search.
Proof completed.
```
```Abella < Theorem ho2db_det1 :
forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D} -> {L |- ho2db M2 H D} ->
M1 =
M2.

```
```
============================
forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D} -> {L |- ho2db M2 H D} ->
M1 =
M2

ho2db_det1 < induction on 2.
```
```
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
============================
forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}@ ->
{L |- ho2db M2 H D} -> M1 =
M2

ho2db_det1 < intros.
```
```
Variables: L M1 M2 D H
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H2 : {L |- ho2db M1 H D}@
H3 : {L |- ho2db M2 H D}
============================
M1 = M2

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

Variables: L M2 H DN N DM M
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H3 : {L |- ho2db M2 H (dapp DM DN)}
H4 : {L |- ho2db M H DM}*
H5 : {L |- ho2db N H DN}*
============================
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

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

Variables: L H DN N DM M N1 M3
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- ho2db M H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L |- ho2db M3 H DM}
H7 : {L |- ho2db N1 H DN}
============================
app M N = app M3 N1

Subgoal 1.2 is:
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply IH to H1 H4 H6.
```
```Subgoal 1.1:

Variables: L H DN N DM N1 M3
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- ho2db M3 H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L |- ho2db M3 H DM}
H7 : {L |- ho2db N1 H DN}
============================
app M3 N = app M3 N1

Subgoal 1.2 is:
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply IH to H1 H5 H7.
```
```Subgoal 1.1:

Variables: L H DN DM N1 M3
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- ho2db M3 H DM}*
H5 : {L |- ho2db N1 H DN}*
H6 : {L |- ho2db M3 H DM}
H7 : {L |- ho2db N1 H DN}
============================
app M3 N1 = app M3 N1

Subgoal 1.2 is:
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < search.
```
```Subgoal 1.2:

Variables: L M2 H DN N DM M F
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- ho2db M H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L, [F] |- ho2db M2 H (dapp DM DN)}
H7 : member F L
============================
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply ctx_world to H1 H7.
```
```Subgoal 1.2:

Variables: L M2 H DN N DM M X HX
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- ho2db M H DM}*
H5 : {L |- ho2db N H DN}*
H6 : {L, [depth X HX] |- ho2db M2 H (dapp DM DN)}
H7 : member (depth X HX) L
H8 : name X
============================
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < case H6.
```
```Subgoal 2:

Variables: L M2 H DR R
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H3 : {L |- ho2db M2 H (dlam DR)}
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
============================
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

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

Variables: L H DR R R1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, depth n1 H |- ho2db (R1 n1) (s H) DR}
============================
lam R = lam R1

Subgoal 2.2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply ctx_nat to H1.
```
```Subgoal 2.1:

Variables: L H DR R R1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, depth n1 H |- ho2db (R1 n1) (s H) DR}
H6 : nat H
============================
lam R = lam R1

Subgoal 2.2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply IH to _ H4 H5.
```
```Subgoal 2.1:

Variables: L H DR R1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R1 n1) (s H) DR}*
H5 : {L, depth n1 H |- ho2db (R1 n1) (s H) DR}
H6 : nat H
============================
lam (z1\R1 z1) = lam R1

Subgoal 2.2 is:
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < search.
```
```Subgoal 2.2:

Variables: L M2 H DR R F
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, [F] |- ho2db M2 H (dlam DR)}
H6 : member F L
============================
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply ctx_world to H1 H6.
```
```Subgoal 2.2:

Variables: L M2 H DR R X HX
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L, depth n1 H |- ho2db (R n1) (s H) DR}*
H5 : {L, [depth X HX] |- ho2db M2 H (dlam DR)}
H6 : member (depth X HX) L
H7 : name X
============================
lam R = M2

Subgoal 3 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < case H5.
```
```Subgoal 3:

Variables: L M1 M2 H DX HX
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H3 : {L |- ho2db M2 H (dvar DX)}
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
============================
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < case H3.
```
```Subgoal 3.1:

Variables: L M1 M2 H DX HX HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- depth M2 HX1}
H7 : {L |- add HX1 DX H}
============================
M1 = M2

Subgoal 3.2 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply add_ignores_ctx to H1 H5.
```
```Subgoal 3.1:

Variables: L M1 M2 H DX HX HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- depth M2 HX1}
H7 : {L |- add HX1 DX H}
H8 : {add HX DX H}
============================
M1 = M2

Subgoal 3.2 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply add_ignores_ctx to H1 H7.
```
```Subgoal 3.1:

Variables: L M1 M2 H DX HX HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- depth M2 HX1}
H7 : {L |- add HX1 DX H}
H8 : {add HX DX H}
H9 : {add HX1 DX H}
============================
M1 = M2

Subgoal 3.2 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply ctx_nat to H1.
```
```Subgoal 3.1:

Variables: L M1 M2 H DX HX HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
H6 : {L |- depth M2 HX1}
H7 : {L |- add HX1 DX H}
H8 : {add HX DX H}
H9 : {add HX1 DX H}
H10 : nat H
============================
M1 = M2

Subgoal 3.2 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply add_det1 to H10 H8 H9.
```
```Subgoal 3.1:

Variables: L M1 M2 H DX HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX1}*
H5 : {L |- add HX1 DX H}*
H6 : {L |- depth M2 HX1}
H7 : {L |- add HX1 DX H}
H8 : {add HX1 DX H}
H9 : {add HX1 DX H}
H10 : nat H
============================
M1 = M2

Subgoal 3.2 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply depth_det1 to H1 H4 H6.
```
```Subgoal 3.1:

Variables: L M2 H DX HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M2 HX1}*
H5 : {L |- add HX1 DX H}*
H6 : {L |- depth M2 HX1}
H7 : {L |- add HX1 DX H}
H8 : {add HX1 DX H}
H9 : {add HX1 DX H}
H10 : nat H
============================
M2 = M2

Subgoal 3.2 is:
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < search.
```
```Subgoal 3.2:

Variables: L M1 M2 H DX HX F
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
H6 : {L, [F] |- ho2db M2 H (dvar DX)}
H7 : member F L
============================
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < apply ctx_world to H1 H7.
```
```Subgoal 3.2:

Variables: L M1 M2 H DX HX X HX1
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H4 : {L |- depth M1 HX}*
H5 : {L |- add HX DX H}*
H6 : {L, [depth X HX1] |- ho2db M2 H (dvar DX)}
H7 : member (depth X HX1) L
H8 : name X
============================
M1 = M2

Subgoal 4 is:
M1 = M2

ho2db_det1 < case H6.
```
```Subgoal 4:

Variables: L M1 M2 D H F
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H3 : {L |- ho2db M2 H D}
H4 : {L, [F] |- ho2db M1 H D}*
H5 : member F L
============================
M1 = M2

ho2db_det1 < apply ctx_world to H1 H5.
```
```Subgoal 4:

Variables: L M1 M2 D H X HX
IH : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D}* ->
{L |- ho2db M2 H D} -> M1 =
M2
H1 : ctx L H
H3 : {L |- ho2db M2 H D}
H4 : {L, [depth X HX] |- ho2db M1 H D}*
H5 : member (depth X HX) L
H6 : name X
============================
M1 = M2

ho2db_det1 < case H4.
Proof completed.
```
```Abella < Theorem ho2db_det1_simple :
forall M1 M2 D, {ho2db M1 z D} -> {ho2db M2 z D} -> M1 = M2.

```
```
============================
forall M1 M2 D, {ho2db M1 z D} -> {ho2db M2 z D} -> M1 = M2

ho2db_det1_simple < intros.
```
```
Variables: M1 M2 D
H1 : {ho2db M1 z D}
H2 : {ho2db M2 z D}
============================
M1 = M2

ho2db_det1_simple < apply ho2db_det1 to _ H1 H2.
```
```
Variables: M2 D
H1 : {ho2db M2 z D}
H2 : {ho2db M2 z D}
============================
M2 = M2

ho2db_det1_simple < search.
Proof completed.
```
```Abella <
```