Welcome to Abella 2.0.5-dev.
Abella < Specification "debruijn".
Reading 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

add_le < induction on 1.

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

add_le < intros.

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

add_le < case H1.
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)

add_le < search.
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)

add_le < search.
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

add_absurd < intros.

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

add_absurd < apply add_le to H2.

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

add_zero < intros.

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

add_zero < case H2.
Subgoal 1:

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

Subgoal 2 is:
 s A1 = z

add_zero < search.
Subgoal 2:

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

add_zero < case H1.
Subgoal 2:

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

add_zero < apply add_absurd to H4 H3.
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

add_det1 < induction on 2.

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

add_det1 < intros.

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

add_det1 < case H2.
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

add_det1 < apply add_zero to H1 H3.
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

add_det1 < search.
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

add_det1 < case H3.
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

add_det1 < case H1.
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

add_det1 < apply add_absurd to H5 H4.
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

add_det1 < case H1.
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

add_det1 < search.
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

add_det2 < induction on 1.

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

add_det2 < intros.

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

add_det2 < case H1.
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

add_det2 < case H2.
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

add_det2 < search.
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

add_det2 < case H2.
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

add_det2 < search.
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}

add_ignores_ctx < induction on 2.

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}

add_ignores_ctx < intros.

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}@
============================
 {add A B C}

add_ignores_ctx < case H2.
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
============================
 {add z C C}

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

Subgoal 3 is:
 {add A B C}

add_ignores_ctx < search.
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 A B C}

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:
 {add A B C}

add_ignores_ctx < search.
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 A B C}

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
============================
 {add A B C}

add_ignores_ctx < case H3.
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 <