Welcome to Abella 2.0.5-dev.
Abella < Specification "debruijn_ho".


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 ((pi H'\pi DX\add H DX H' => ho2db x H' (dvar DX)) :: 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_inv :
forall E L H, ctx L H -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H).



============================
forall E L H, ctx L H -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)

ctx_inv < induction on 1.


IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
============================
forall E L H, ctx L H @ -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)

ctx_inv < intros.


Variables: E L H
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H1 : ctx L H @
H2 : member E L
============================
exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H

ctx_inv < case H1.

Subgoal 1:

Variables: E
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H2 : member E nil
============================
exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) z

Subgoal 2 is:
exists X HX, E n1 = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) (s H1)

ctx_inv < case H2.

Subgoal 2:

Variables: E H1 L1
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H2 : member (E n1)
((pi H'\pi DX\add H1 DX H' => ho2db n1 H' (dvar DX)) :: L1)
H3 : ctx L1 H1 *
============================
exists X HX, E n1 = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) (s H1)

ctx_inv < case H2.

Subgoal 2.1:

Variables: H1 L1
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H3 : ctx L1 H1 *
============================
exists X HX, pi H'\pi DX\add H1 DX H' => ho2db n1 H' (dvar DX) =
pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\ name X /\
le (s HX) (s H1)

Subgoal 2.2 is:
exists X HX, E n1 = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) (s H1)

ctx_inv < search.

Subgoal 2.2:

Variables: E H1 L1
IH : forall E L H, ctx L H * -> member E L ->
(exists X HX, E = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H3 : ctx L1 H1 *
H4 : member (E n1) L1
============================
exists X HX, E n1 = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) (s H1)

ctx_inv < 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 = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H3 : ctx L1 H1 *
H4 : member F L1
============================
exists X HX, F = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) (s H1)

ctx_inv < 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 = pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) /\
name X /\ le (s HX) H)
H3 : ctx L1 H1 *
H4 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L1
H5 : name X
H6 : le (s HX) H1
============================
exists X1 HX1, pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX) =
pi H'\pi DX\add HX1 DX H' => ho2db X1 H' (dvar DX) /\ name X1 /\
le (s HX1) (s H1)

ctx_inv < search.
Proof completed.

Abella < Theorem ctx_unique1 :
forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2.



============================
forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2

ctx_unique1 < induction on 2.


IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
============================
forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L @ ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2

ctx_unique1 < intros.


Variables: L H X H1 H2
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx L H
H2 : member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L @
H3 : member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L
============================
H1 = H2

ctx_unique1 < case H2.

Subgoal 1:

Variables: H X H1 H2 L1
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx ((pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) :: L1) H
H3 : member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX))
((pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) :: L1)
============================
H1 = H2

Subgoal 2 is:
H1 = H2

ctx_unique1 < case H3.

Subgoal 1.1:

Variables: H X H1 L1
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx ((pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) :: L1) H
============================
H1 = H1

Subgoal 1.2 is:
H1 = H2

Subgoal 2 is:
H1 = H2

ctx_unique1 < search.

Subgoal 1.2:

Variables: H X H1 H2 L1
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx ((pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) :: L1) H
H4 : member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L1
============================
H1 = H2

Subgoal 2 is:
H1 = H2

ctx_unique1 < case H1.

Subgoal 1.2:

Variables: H2 H3 L2
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H4 : member (pi H'\pi DX\add (H2 n1) DX H' => ho2db n1 H' (dvar DX)) L2
H5 : ctx L2 H3
============================
H3 = H2 n1

Subgoal 2 is:
H1 = H2

ctx_unique1 < 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 (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx (B :: L1) H
H3 : member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) (B :: L1)
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L1 *
============================
H1 = H2

ctx_unique1 < case H3.

Subgoal 2.1:

Variables: H X H1 H2 L1
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx ((pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) :: L1) H
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L1 *
============================
H1 = H2

Subgoal 2.2 is:
H1 = H2

ctx_unique1 < case H1.

Subgoal 2.1:

Variables: H1 H3 L2
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H4 : member (pi H'\pi DX\add (H1 n1) DX H' => ho2db n1 H' (dvar DX)) L2 *
H5 : ctx L2 H3
============================
H1 n1 = H3

Subgoal 2.2 is:
H1 = H2

ctx_unique1 < 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 (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H1 : ctx (B :: L1) H
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L1 *
H5 : member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L1
============================
H1 = H2

ctx_unique1 < case H1.

Subgoal 2.2:

Variables: X H1 H2 H3 L2
IH : forall L H X H1 H2, ctx L H ->
member (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H4 : member (pi H'\pi DX\add (H1 n1) DX H' => ho2db (X n1) H' (dvar DX)) L2 *
H5 : member (pi H'\pi DX\add (H2 n1) DX H' => ho2db (X n1) H' (dvar DX)) L2
H6 : ctx L2 H3
============================
H1 n1 = H2 n1

ctx_unique1 < 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 (pi H'\pi DX\add H1 DX H' => ho2db X H' (dvar DX)) L * ->
member (pi H'\pi DX\add H2 DX H' => ho2db X H' (dvar DX)) L -> H1 =
H2
H4 : member (pi H'\pi DX\add (H2 n1) DX H' => ho2db (X n1) H' (dvar DX)) L2 *
H5 : member (pi H'\pi DX\add (H2 n1) DX H' => ho2db (X n1) H' (dvar DX)) L2
H6 : ctx L2 H3
============================
H2 n1 = H2 n1

ctx_unique1 < search.
Proof completed.

Abella < Theorem ctx_unique2 :
forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2.



============================
forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2

ctx_unique2 < induction on 2.


IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
============================
forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L @ ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2

ctx_unique2 < intros.


Variables: L H X1 X2 HX
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx L H
H2 : member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L @
H3 : member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L
============================
X1 = X2

ctx_unique2 < case H2.

Subgoal 1:

Variables: H X1 X2 HX L1
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx ((pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) :: L1) H
H3 : member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX))
((pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) :: L1)
============================
X1 = X2

Subgoal 2 is:
X1 = X2

ctx_unique2 < case H3.

Subgoal 1.1:

Variables: H X1 HX L1
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx ((pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) :: L1) H
============================
X1 = X1

Subgoal 1.2 is:
X1 = X2

Subgoal 2 is:
X1 = X2

ctx_unique2 < search.

Subgoal 1.2:

Variables: H X1 X2 HX L1
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx ((pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) :: L1) H
H4 : member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L1
============================
X1 = X2

Subgoal 2 is:
X1 = X2

ctx_unique2 < case H1.

Subgoal 1.2:

Variables: X2 H1 L2
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db (X2 n1) H' (dvar DX)) L2
H5 : ctx L2 H1
============================
n1 = X2 n1

Subgoal 2 is:
X1 = X2

ctx_unique2 < apply ctx_inv to H5 H4.

Subgoal 1.2:

Variables: H1 L2 X
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db (X n1) H' (dvar DX)) L2
H5 : ctx L2 H1
H6 : name (X n1)
H7 : le (s H1) H1
============================
n1 = X n1

Subgoal 2 is:
X1 = X2

ctx_unique2 < apply ctx_nat to H5.

Subgoal 1.2:

Variables: H1 L2 X
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db (X n1) H' (dvar DX)) L2
H5 : ctx L2 H1
H6 : name (X n1)
H7 : le (s H1) H1
H8 : nat H1
============================
n1 = X n1

Subgoal 2 is:
X1 = X2

ctx_unique2 < apply le_absurd to H8 H7.

Subgoal 2:

Variables: H X1 X2 HX L1 B
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx (B :: L1) H
H3 : member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) (B :: L1)
H4 : member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L1 *
============================
X1 = X2

ctx_unique2 < case H3.

Subgoal 2.1:

Variables: H X1 X2 HX L1
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx ((pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) :: L1) H
H4 : member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L1 *
============================
X1 = X2

Subgoal 2.2 is:
X1 = X2

ctx_unique2 < case H1.

Subgoal 2.1:

Variables: X1 H1 L2
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db (X1 n1) H' (dvar DX)) L2 *
H5 : ctx L2 H1
============================
X1 n1 = n1

Subgoal 2.2 is:
X1 = X2

ctx_unique2 < apply ctx_inv to H5 H4.

Subgoal 2.1:

Variables: H1 L2 X
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db (X n1) H' (dvar DX)) L2 *
H5 : ctx L2 H1
H6 : name (X n1)
H7 : le (s H1) H1
============================
X n1 = n1

Subgoal 2.2 is:
X1 = X2

ctx_unique2 < apply ctx_nat to H5.

Subgoal 2.1:

Variables: H1 L2 X
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add H1 DX H' => ho2db (X n1) H' (dvar DX)) L2 *
H5 : ctx L2 H1
H6 : name (X n1)
H7 : le (s H1) H1
H8 : nat H1
============================
X n1 = n1

Subgoal 2.2 is:
X1 = X2

ctx_unique2 < apply le_absurd to H8 H7.

Subgoal 2.2:

Variables: H X1 X2 HX L1 B
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H1 : ctx (B :: L1) H
H4 : member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L1 *
H5 : member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L1
============================
X1 = X2

ctx_unique2 < case H1.

Subgoal 2.2:

Variables: X1 X2 HX H1 L2
IH : forall L H X1 X2 HX, ctx L H ->
member (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add (HX n1) DX H' => ho2db (X1 n1) H' (dvar DX)) L2 *
H5 : member (pi H'\pi DX\add (HX n1) DX H' => ho2db (X2 n1) H' (dvar DX)) L2
H6 : ctx L2 H1
============================
X1 n1 = X2 n1

ctx_unique2 < 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 (pi H'\pi DX\add HX DX H' => ho2db X1 H' (dvar DX)) L * ->
member (pi H'\pi DX\add HX DX H' => ho2db X2 H' (dvar DX)) L -> X1 =
X2
H4 : member (pi H'\pi DX\add (HX n1) DX H' => ho2db (X2 n1) H' (dvar DX)) L2 *
H5 : member (pi H'\pi DX\add (HX n1) DX H' => ho2db (X2 n1) H' (dvar DX)) L2
H6 : ctx L2 H1
============================
X2 n1 = X2 n1

ctx_unique2 < 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_inv 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, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |- add A B C}*
H4 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H5 : name X
H6 : le (s HX) H
============================

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:
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 = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 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 = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 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 = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
D1 = D2

ho2db_det3 < search.

Subgoal 1.2:

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:
D1 = D2

ho2db_det3 < apply ctx_inv to H1 H7.

Subgoal 1.2:

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, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |-
ho2db (app M1 N) H D2}
H7 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H8 : name X
H9 : le (s HX) H
============================
dapp DM DN = D2

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
D1 = D2

ho2db_det3 < case H6.

Subgoal 1.2:

Variables: L H DN N DM M1 HX DX
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}*
H7 : member (pi H'\pi DX\add HX DX H' => ho2db (app M1 N) H' (dvar DX)) L
H8 : name (app M1 N)
H9 : le (s HX) H
H10 : {L |- add HX DX H}
============================
dapp DM DN = dvar DX

Subgoal 2 is:
dlam DR = D2

Subgoal 3 is:
D1 = D2

ho2db_det3 < case H8.

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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
============================
dlam DR = D2

Subgoal 3 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
H5 : {L, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR1}
============================
dlam DR = dlam DR1

Subgoal 2.2 is:
dlam DR = D2

Subgoal 3 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR1}*
H5 : {L, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR1}
============================
dlam DR1 = dlam DR1

Subgoal 2.2 is:
dlam DR = D2

Subgoal 3 is:
D1 = D2

ho2db_det3 < search.

Subgoal 2.2:

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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
H5 : {L, [F] |- ho2db (lam R) H D2}
H6 : member F L
============================
dlam DR = D2

Subgoal 3 is:
D1 = D2

ho2db_det3 < apply ctx_inv to H1 H6.

Subgoal 2.2:

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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
H5 : {L, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |-
ho2db (lam R) H D2}
H6 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H7 : name X
H8 : le (s HX) H
============================
dlam DR = D2

Subgoal 3 is:
D1 = D2

ho2db_det3 < case H5.

Subgoal 2.2:

Variables: L H DR R HX DX
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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
H6 : member (pi H'\pi DX\add HX DX H' => ho2db (lam R) H' (dvar DX)) L
H7 : name (lam R)
H8 : le (s HX) H
H9 : {L |- add HX DX H}
============================
dlam DR = dvar DX

Subgoal 3 is:
D1 = D2

ho2db_det3 < case H7.

Subgoal 3:

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_inv to H1 H5.

Subgoal 3:

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, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |- ho2db M H D1}*
H5 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H6 : name X
H7 : le (s HX) H
============================
D1 = D2

ho2db_det3 < case H4.

Subgoal 3:

Variables: L M D2 H HX DX
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}
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
============================
dvar DX = D2

ho2db_det3 < case H3.

Subgoal 3.1:

Variables: L H HX DX 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db (app M1 N) H' (dvar DX)) L
H6 : name (app M1 N)
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H9 : {L |- ho2db M1 H DM}
H10 : {L |- ho2db N H DN}
============================
dvar DX = dapp DM DN

Subgoal 3.2 is:
dvar DX = dlam DR

Subgoal 3.3 is:
dvar DX = D2

ho2db_det3 < case H6.

Subgoal 3.2:

Variables: L H HX DX 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db (lam R) H' (dvar DX)) L
H6 : name (lam R)
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H9 : {L, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}
============================
dvar DX = dlam DR

Subgoal 3.3 is:
dvar DX = D2

ho2db_det3 < case H6.

Subgoal 3.3:

Variables: L M D2 H HX DX F1
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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H9 : {L, [F1] |- ho2db M H D2}
H10 : member F1 L
============================
dvar DX = D2

ho2db_det3 < apply ctx_inv to H1 H10.

Subgoal 3.3:

Variables: L M D2 H HX DX X1 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H9 : {L, [pi H'\pi DX\add HX1 DX H' => ho2db X1 H' (dvar DX)] |-
ho2db M H D2}
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db X1 H' (dvar DX)) L
H11 : name X1
H12 : le (s HX1) H
============================
dvar DX = D2

ho2db_det3 < case H9.

Subgoal 3.3:

Variables: L M H HX DX HX1 DX1
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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H11 : name M
H12 : le (s HX1) H
H13 : {L |- add HX1 DX1 H}
============================
dvar DX = dvar DX1

ho2db_det3 < apply ctx_unique1 to H1 H5 H10.

Subgoal 3.3:

Variables: L M H DX HX1 DX1
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
H5 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX1) H
H8 : {L |- add HX1 DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H11 : name M
H12 : le (s HX1) H
H13 : {L |- add HX1 DX1 H}
============================
dvar DX = dvar DX1

ho2db_det3 < apply add_ignores_ctx to H1 H8.

Subgoal 3.3:

Variables: L M H DX HX1 DX1
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
H5 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX1) H
H8 : {L |- add HX1 DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H11 : name M
H12 : le (s HX1) H
H13 : {L |- add HX1 DX1 H}
H14 : {add HX1 DX H}
============================
dvar DX = dvar DX1

ho2db_det3 < apply add_ignores_ctx to H1 H13.

Subgoal 3.3:

Variables: L M H DX HX1 DX1
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
H5 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX1) H
H8 : {L |- add HX1 DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H11 : name M
H12 : le (s HX1) H
H13 : {L |- add HX1 DX1 H}
H14 : {add HX1 DX H}
H15 : {add HX1 DX1 H}
============================
dvar DX = dvar DX1

ho2db_det3 < apply add_det2 to H14 H15.

Subgoal 3.3:

Variables: L M H HX1 DX1
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
H5 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H6 : name M
H7 : le (s HX1) H
H8 : {L |- add HX1 DX1 H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M H' (dvar DX)) L
H11 : name M
H12 : le (s HX1) H
H13 : {L |- add HX1 DX1 H}
H14 : {add HX1 DX1 H}
H15 : {add HX1 DX1 H}
============================
dvar DX1 = dvar DX1

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

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

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

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

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

ho2db_det1 < apply ctx_inv 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, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |-
ho2db M2 H (dapp DM DN)}
H7 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H8 : name X
H9 : le (s HX) H
============================
app M N = M2

Subgoal 2 is:
lam R = M2

Subgoal 3 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
============================
lam R = M2

Subgoal 3 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
H5 : {L, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R1 n1) (s H) DR}
============================
lam R = lam R1

Subgoal 2.2 is:
lam R = M2

Subgoal 3 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R1 n1) (s H) DR}*
H5 : {L, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R1 n1) (s H) DR}
============================
lam (z1\R1 z1) = lam R1

Subgoal 2.2 is:
lam R = M2

Subgoal 3 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
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

ho2db_det1 < apply ctx_inv 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, pi H'\pi DX\add H DX H' => ho2db n1 H' (dvar DX) |-
ho2db (R n1) (s H) DR}*
H5 : {L, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |-
ho2db M2 H (dlam DR)}
H6 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H7 : name X
H8 : le (s HX) H
============================
lam R = M2

Subgoal 3 is:
M1 = M2

ho2db_det1 < case H5.

Subgoal 3:

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_inv to H1 H5.

Subgoal 3:

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, [pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)] |- ho2db M1 H D}*
H5 : member (pi H'\pi DX\add HX DX H' => ho2db X H' (dvar DX)) L
H6 : name X
H7 : le (s HX) H
============================
M1 = M2

ho2db_det1 < case H4.

Subgoal 3:

Variables: L M1 M2 H HX DX
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)}
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
============================
M1 = M2

ho2db_det1 < case H3.

Subgoal 3:

Variables: L M1 M2 H HX DX F1
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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H9 : {L, [F1] |- ho2db M2 H (dvar DX)}
H10 : member F1 L
============================
M1 = M2

ho2db_det1 < apply ctx_inv to H1 H10.

Subgoal 3:

Variables: L M1 M2 H HX DX X1 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H9 : {L, [pi H'\pi DX\add HX1 DX H' => ho2db X1 H' (dvar DX)] |-
ho2db M2 H (dvar DX)}
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db X1 H' (dvar DX)) L
H11 : name X1
H12 : le (s HX1) H
============================
M1 = M2

ho2db_det1 < case H9.

Subgoal 3:

Variables: L M1 M2 H HX 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H11 : name M2
H12 : le (s HX1) H
H13 : {L |- add HX1 DX H}
============================
M1 = M2

ho2db_det1 < apply add_ignores_ctx to H1 H8.

Subgoal 3:

Variables: L M1 M2 H HX 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H11 : name M2
H12 : le (s HX1) H
H13 : {L |- add HX1 DX H}
H14 : {add HX DX H}
============================
M1 = M2

ho2db_det1 < apply add_ignores_ctx to H1 H13.

Subgoal 3:

Variables: L M1 M2 H HX 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H11 : name M2
H12 : le (s HX1) H
H13 : {L |- add HX1 DX H}
H14 : {add HX DX H}
H15 : {add HX1 DX H}
============================
M1 = M2

ho2db_det1 < apply ctx_nat to H1.

Subgoal 3:

Variables: L M1 M2 H HX 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
H5 : member (pi H'\pi DX\add HX DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX) H
H8 : {L |- add HX DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H11 : name M2
H12 : le (s HX1) H
H13 : {L |- add HX1 DX H}
H14 : {add HX DX H}
H15 : {add HX1 DX H}
H16 : nat H
============================
M1 = M2

ho2db_det1 < apply add_det1 to H16 H14 H15.

Subgoal 3:

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
H5 : member (pi H'\pi DX\add HX1 DX H' => ho2db M1 H' (dvar DX)) L
H6 : name M1
H7 : le (s HX1) H
H8 : {L |- add HX1 DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H11 : name M2
H12 : le (s HX1) H
H13 : {L |- add HX1 DX H}
H14 : {add HX1 DX H}
H15 : {add HX1 DX H}
H16 : nat H
============================
M1 = M2

ho2db_det1 < apply ctx_unique2 to H1 H5 H10.

Subgoal 3:

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
H5 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H6 : name M2
H7 : le (s HX1) H
H8 : {L |- add HX1 DX H}*
H10 : member (pi H'\pi DX\add HX1 DX H' => ho2db M2 H' (dvar DX)) L
H11 : name M2
H12 : le (s HX1) H
H13 : {L |- add HX1 DX H}
H14 : {add HX1 DX H}
H15 : {add HX1 DX H}
H16 : nat H
============================
M2 = M2

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