Welcome to Abella 2.0.2-lf

Abella < Specification "debruijn.elf".
Reading specification "debruijn.elf"
sig debruijn.
  type nat lftype.
  type z lfobj.
  type s lfobj -> lfobj.
  type add lfobj -> lfobj -> lfobj -> lftype.
  type add/z lfobj -> lfobj.
  type add/s lfobj -> lfobj -> lfobj -> lfobj -> lfobj.
  type hterm lftype.
  type happ lfobj -> lfobj -> lfobj.
  type hlam (lfobj -> lfobj) -> lfobj.
  type dterm lftype.
  type dapp lfobj -> lfobj -> lfobj.
  type dlam lfobj -> lfobj.
  type dvar lfobj -> lfobj.
  type ho2db lfobj -> lfobj -> lfobj -> lftype.
  type ho2db/app lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj.
  type ho2db/lam (lfobj -> lfobj) -> lfobj -> lfobj -> (lfobj -> (lfobj -> lfobj -> lfobj -> lfobj) -> lfobj) -> lfobj.
end.
module debruijn.
  (* nat:type *)
  lfisty nat.
  (* z:nat *)
  lfhas z nat.
  (* s:nat -> nat *)
  pi lf_1\lfhas lf_1 nat => lfhas (s lf_1) nat.
  (* add:nat -> nat -> nat -> type *)
  pi lf_1\lfhas lf_1 nat =>
    pi lf_2\lfhas lf_2 nat =>
      pi lf_3\lfhas lf_3 nat => lfisty (add lf_1 lf_2 lf_3).
  (* add/z:{C:nat} add z C C *)
  pi C\lfhas C nat => lfhas (add/z C) (add z C C).
  (* add/s:{A:nat} {B:nat} {C:nat} add A B C -> add (s A) B (s C) *)
  pi A\lfhas A nat =>
    pi B\lfhas B nat =>
      pi C\lfhas C nat =>
        pi lf_1\lfhas lf_1 (add A B C) =>
          lfhas (add/s A B C lf_1) (add (s A) B (s C)).
  (* hterm:type *)
  lfisty hterm.
  (* happ:hterm -> hterm -> hterm *)
  pi lf_1\lfhas lf_1 hterm =>
    pi lf_2\lfhas lf_2 hterm => lfhas (happ lf_1 lf_2) hterm.
  (* hlam:(hterm -> hterm) -> hterm *)
  pi lf_1\(pi lf_2\lfhas lf_2 hterm => lfhas (lf_1 lf_2) hterm) =>
    lfhas (hlam lf_1) hterm.
  (* dterm:type *)
  lfisty dterm.
  (* dapp:dterm -> dterm -> dterm *)
  pi lf_1\lfhas lf_1 dterm =>
    pi lf_2\lfhas lf_2 dterm => lfhas (dapp lf_1 lf_2) dterm.
  (* dlam:dterm -> dterm *)
  pi lf_1\lfhas lf_1 dterm => lfhas (dlam lf_1) dterm.
  (* dvar:nat -> dterm *)
  pi lf_1\lfhas lf_1 nat => lfhas (dvar lf_1) dterm.
  (* ho2db:hterm -> nat -> dterm -> type *)
  pi lf_1\lfhas lf_1 hterm =>
    pi lf_2\lfhas lf_2 nat =>
      pi lf_3\lfhas lf_3 dterm => lfisty (ho2db lf_1 lf_2 lf_3).
  (* ho2db/app:{M:hterm} {N:hterm} {H:nat} {DM:dterm} {DN:dterm}
       ho2db M H DM -> ho2db N H DN -> ho2db (happ M N) H (dapp DM DN) *)
  pi M\lfhas M hterm =>
    pi N\lfhas N hterm =>
      pi H\lfhas H nat =>
        pi DM\lfhas DM dterm =>
          pi DN\lfhas DN dterm =>
            pi lf_1\lfhas lf_1 (ho2db M H DM) =>
              pi lf_2\lfhas lf_2 (ho2db N H DN) =>
                lfhas (ho2db/app M N H DM DN lf_1 lf_2)
                  (ho2db (happ M N) H (dapp DM DN)).
  (* ho2db/lam:{R:hterm -> hterm} {H:nat} {DR:dterm}
       ({x:hterm} ({hh:nat} {dx:nat} add H dx hh -> ho2db x hh (dvar dx)) ->
          ho2db (R x) (s H) DR) ->
       ho2db (hlam R) H (dlam DR) *)
  pi R\(pi lf_1\lfhas lf_1 hterm => lfhas (R lf_1) hterm) =>
    pi H\lfhas H nat =>
      pi DR\lfhas DR dterm =>
        pi lf_1\(pi x\lfhas x hterm =>
                   pi lf_2\(pi hh\lfhas hh nat =>
                              pi dx\lfhas dx nat =>
                                pi lf_3\lfhas lf_3 (add H dx hh) =>
                                  lfhas (lf_2 hh dx lf_3)
                                    (ho2db x hh (dvar dx))) =>
                     lfhas (lf_1 x lf_2) (ho2db (R x) (s H) DR)) =>
          lfhas (ho2db/lam R H DR lf_1) (ho2db (hlam R) H (dlam DR)).
end.

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 < Theorem member_prune3 : 
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_prune3 < 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_prune3 < 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_prune3 < 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_prune3 < 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_prune3 < 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_prune3 < search.
Proof completed.

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

Abella < Theorem le_decr : 
forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y -> le X Y.

============================
 forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y -> le X Y

le_decr < induction on 3.

IH : forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y * -> le X Y
============================
 forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y @ -> le X Y

le_decr < intros.

Variables: X Y
IH : forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y * -> le X Y
H1 : <X:nat>
H2 : <Y:nat>
H3 : le (s X) Y @
============================
 le X Y

le_decr < case H3.

Subgoal 1:

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

Subgoal 2 is:
 le X (s Y1)

le_decr < search.

Subgoal 2:

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

le_decr < case H2.

Subgoal 2:

Variables: X Y1
IH : forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y * -> le X Y
H1 : <X:nat>
H4 : le (s X) Y1 *
H5 : <Y1:nat>
============================
 le X (s Y1)

le_decr < apply IH to _ _ H4.

Subgoal 2:

Variables: X Y1
IH : forall X Y, <X:nat> -> <Y:nat> -> le (s X) Y * -> le X Y
H1 : <X:nat>
H4 : le (s X) Y1 *
H5 : <Y1:nat>
H6 : le X Y1
============================
 le X (s Y1)

le_decr < search.
Proof completed.

Abella < Theorem le_absurd : 
forall X, <X:nat> -> ~ le (s X) X.

============================
 forall X, <X:nat> -> ~ le (s X) X

le_absurd < induction on 1.

IH : forall X, <X:nat>* -> ~ le (s X) X
============================
 forall X, <X:nat>@ -> ~ le (s X) X

le_absurd < intros.

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

le_absurd < case H1.

Subgoal 1:

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

Subgoal 2 is:
 false

le_absurd < case H2.

Subgoal 2:

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

le_absurd < case H2.

Subgoal 2:

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

le_absurd < apply le_decr to _ _ H4.

Subgoal 2:

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

le_absurd < apply IH to H3 H5.
Proof completed.

Abella < Theorem add_le : 
forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C> -> le B C.

============================
 forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C> -> le B C

add_le < induction on 4.

IH : forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>* ->
       le B C
============================
 forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>@ -> le B C

add_le < intros.

Variables: A B C P
IH : forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>* ->
       le B C
H1 : <A:nat>
H2 : <B:nat>
H3 : <C:nat>
H4 : <P:add A B C>@
============================
 le B C

add_le < case H4.

Subgoal 1:

Variables: C
IH : forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>* ->
       le B C
H1 : <z:nat>
H2 : <C:nat>
H3 : <C:nat>
H5 : <C:nat>*
============================
 le C C

Subgoal 2 is:
 le B (s C1)

add_le < search.

Subgoal 2:

Variables: B C1 A1 lf_1
IH : forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>* ->
       le B C
H1 : <s A1:nat>
H2 : <B:nat>
H3 : <s C1:nat>
H5 : <A1:nat>*
H6 : <B:nat>*
H7 : <C1:nat>*
H8 : <lf_1:add A1 B C1>*
============================
 le B (s C1)

add_le < case H3.

Subgoal 2:

Variables: B C1 A1 lf_1
IH : forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>* ->
       le B C
H1 : <s A1:nat>
H2 : <B:nat>
H5 : <A1:nat>*
H6 : <B:nat>*
H7 : <C1:nat>*
H8 : <lf_1:add A1 B C1>*
H9 : <C1:nat>
============================
 le B (s C1)

add_le < apply IH to _ _ _ H8.

Subgoal 2:

Variables: B C1 A1 lf_1
IH : forall A B C P, <A:nat> -> <B:nat> -> <C:nat> -> <P:add A B C>* ->
       le B C
H1 : <s A1:nat>
H2 : <B:nat>
H5 : <A1:nat>*
H6 : <B:nat>*
H7 : <C1:nat>*
H8 : <lf_1:add A1 B C1>*
H9 : <C1:nat>
H10 : le B C1
============================
 le B (s C1)

add_le < search.
Proof completed.

Abella < Theorem add_absurd : 
forall A C P, <A:nat> -> <C:nat> -> ~ <P:add A (s C) C>.

============================
 forall A C P, <A:nat> -> <C:nat> -> ~ <P:add A (s C) C>

add_absurd < intros.

Variables: A C P
H1 : <A:nat>
H2 : <C:nat>
H3 : <P:add A (s C) C>
============================
 false

add_absurd < apply add_le to _ _ _ H3.

Variables: A C P
H1 : <A:nat>
H2 : <C:nat>
H3 : <P:add A (s C) C>
H4 : le (s C) C
============================
 false

add_absurd < apply le_absurd to _ H4.
Proof completed.

Abella < Theorem add_zero : 
forall A C P, <A:nat> -> <C:nat> -> <P:add A C C> -> A = z.

============================
 forall A C P, <A:nat> -> <C:nat> -> <P:add A C C> -> A = z

add_zero < intros.

Variables: A C P
H1 : <A:nat>
H2 : <C:nat>
H3 : <P:add A C C>
============================
 A = z

add_zero < case H3.

Subgoal 1:

Variables: C
H1 : <z:nat>
H2 : <C:nat>
H4 : <C:nat>
============================
 z = z

Subgoal 2 is:
 s A1 = z

add_zero < search.

Subgoal 2:

Variables: C1 A1 lf_1
H1 : <s A1:nat>
H2 : <s C1:nat>
H4 : <A1:nat>
H5 : <s C1:nat>
H6 : <C1:nat>
H7 : <lf_1:add A1 (s C1) C1>
============================
 s A1 = z

add_zero < case H2.

Subgoal 2:

Variables: C1 A1 lf_1
H1 : <s A1:nat>
H4 : <A1:nat>
H5 : <s C1:nat>
H6 : <C1:nat>
H7 : <lf_1:add A1 (s C1) C1>
H8 : <C1:nat>
============================
 s A1 = z

add_zero < apply add_absurd to _ _ H7.
Proof completed.

Abella < Theorem add_det1 : 
forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
  <P1:add A1 B C> -> <P2:add A2 B C> -> A1 = A2.

============================
 forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
   <P1:add A1 B C> -> <P2:add A2 B C> -> A1 = A2

add_det1 < induction on 5.

IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
============================
 forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
   <P1:add A1 B C>@ -> <P2:add A2 B C> -> A1 = A2

add_det1 < intros.

Variables: A1 A2 B C P1 P2
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <A1:nat>
H2 : <A2:nat>
H3 : <B:nat>
H4 : <C:nat>
H5 : <P1:add A1 B C>@
H6 : <P2:add A2 B C>
============================
 A1 = A2

add_det1 < case H5.

Subgoal 1:

Variables: A2 C P2
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <z:nat>
H2 : <A2:nat>
H3 : <C:nat>
H4 : <C:nat>
H6 : <P2:add A2 C C>
H7 : <C:nat>*
============================
 z = A2

Subgoal 2 is:
 s A = A2

add_det1 < apply add_zero to _ _ H6.

Subgoal 1:

Variables: C P2
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <z:nat>
H2 : <z:nat>
H3 : <C:nat>
H4 : <C:nat>
H6 : <P2:add z C C>
H7 : <C:nat>*
============================
 z = z

Subgoal 2 is:
 s A = A2

add_det1 < search.

Subgoal 2:

Variables: A2 B P2 C1 A lf_1
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <s A:nat>
H2 : <A2:nat>
H3 : <B:nat>
H4 : <s C1:nat>
H6 : <P2:add A2 B (s C1)>
H7 : <A:nat>*
H8 : <B:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A B C1>*
============================
 s A = A2

add_det1 < case H6.

Subgoal 2.1:

Variables: C1 A lf_1
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <s A:nat>
H2 : <z:nat>
H3 : <s C1:nat>
H4 : <s C1:nat>
H7 : <A:nat>*
H8 : <s C1:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A (s C1) C1>*
H11 : <s C1:nat>
============================
 s A = z

Subgoal 2.2 is:
 s A = s A3

add_det1 < case H4.

Subgoal 2.1:

Variables: C1 A lf_1
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <s A:nat>
H2 : <z:nat>
H3 : <s C1:nat>
H7 : <A:nat>*
H8 : <s C1:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A (s C1) C1>*
H11 : <s C1:nat>
H12 : <C1:nat>
============================
 s A = z

Subgoal 2.2 is:
 s A = s A3

add_det1 < apply add_absurd to _ _ H10.

Subgoal 2.2:

Variables: B C1 A lf_1 A3 lf_2
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <s A:nat>
H2 : <s A3:nat>
H3 : <B:nat>
H4 : <s C1:nat>
H7 : <A:nat>*
H8 : <B:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A B C1>*
H11 : <A3:nat>
H12 : <B:nat>
H13 : <C1:nat>
H14 : <lf_2:add A3 B C1>
============================
 s A = s A3

add_det1 < case H4.

Subgoal 2.2:

Variables: B C1 A lf_1 A3 lf_2
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <s A:nat>
H2 : <s A3:nat>
H3 : <B:nat>
H7 : <A:nat>*
H8 : <B:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A B C1>*
H11 : <A3:nat>
H12 : <B:nat>
H13 : <C1:nat>
H14 : <lf_2:add A3 B C1>
H15 : <C1:nat>
============================
 s A = s A3

add_det1 < apply IH to _ _ _ _ H10 H14.

Subgoal 2.2:

Variables: B C1 lf_1 A3 lf_2
IH : forall A1 A2 B C P1 P2, <A1:nat> -> <A2:nat> -> <B:nat> -> <C:nat> ->
       <P1:add A1 B C>* -> <P2:add A2 B C> -> A1 = A2
H1 : <s A3:nat>
H2 : <s A3:nat>
H3 : <B:nat>
H7 : <A3:nat>*
H8 : <B:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A3 B C1>*
H11 : <A3:nat>
H12 : <B:nat>
H13 : <C1:nat>
H14 : <lf_2:add A3 B C1>
H15 : <C1:nat>
============================
 s A3 = s A3

add_det1 < search.
Proof completed.

Abella < Theorem add_det2 : 
forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
  <P1:add A B1 C> -> <P2:add A B2 C> -> B1 = B2.

============================
 forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
   <P1:add A B1 C> -> <P2:add A B2 C> -> B1 = B2

add_det2 < induction on 5.

IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
============================
 forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
   <P1:add A B1 C>@ -> <P2:add A B2 C> -> B1 = B2

add_det2 < intros.

Variables: A B1 B2 C P1 P2
IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
H1 : <A:nat>
H2 : <B1:nat>
H3 : <B2:nat>
H4 : <C:nat>
H5 : <P1:add A B1 C>@
H6 : <P2:add A B2 C>
============================
 B1 = B2

add_det2 < case H5.

Subgoal 1:

Variables: B2 C P2
IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
H1 : <z:nat>
H2 : <C:nat>
H3 : <B2:nat>
H4 : <C:nat>
H6 : <P2:add z B2 C>
H7 : <C:nat>*
============================
 C = B2

Subgoal 2 is:
 B1 = B2

add_det2 < case H6.

Subgoal 1:

Variables: C
IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
H1 : <z:nat>
H2 : <C:nat>
H3 : <C:nat>
H4 : <C:nat>
H7 : <C:nat>*
H8 : <C:nat>
============================
 C = C

Subgoal 2 is:
 B1 = B2

add_det2 < search.

Subgoal 2:

Variables: B1 B2 P2 C1 A1 lf_1
IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
H1 : <s A1:nat>
H2 : <B1:nat>
H3 : <B2:nat>
H4 : <s C1:nat>
H6 : <P2:add (s A1) B2 (s C1)>
H7 : <A1:nat>*
H8 : <B1:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A1 B1 C1>*
============================
 B1 = B2

add_det2 < case H6.

Subgoal 2:

Variables: B1 B2 C1 A1 lf_1 lf_2
IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
H1 : <s A1:nat>
H2 : <B1:nat>
H3 : <B2:nat>
H4 : <s C1:nat>
H7 : <A1:nat>*
H8 : <B1:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A1 B1 C1>*
H11 : <A1:nat>
H12 : <B2:nat>
H13 : <C1:nat>
H14 : <lf_2:add A1 B2 C1>
============================
 B1 = B2

add_det2 < apply IH to _ _ _ _ H10 H14.

Subgoal 2:

Variables: B2 C1 A1 lf_1 lf_2
IH : forall A B1 B2 C P1 P2, <A:nat> -> <B1:nat> -> <B2:nat> -> <C:nat> ->
       <P1:add A B1 C>* -> <P2:add A B2 C> -> B1 = B2
H1 : <s A1:nat>
H2 : <B2:nat>
H3 : <B2:nat>
H4 : <s C1:nat>
H7 : <A1:nat>*
H8 : <B2:nat>*
H9 : <C1:nat>*
H10 : <lf_1:add A1 B2 C1>*
H11 : <A1:nat>
H12 : <B2:nat>
H13 : <C1:nat>
H14 : <lf_2:add A1 B2 C1>
============================
 B2 = B2

add_det2 < search.
Proof completed.

Abella < Define ctx : olist -> lfobj -> prop by 
ctx nil z;
nabla x p, ctx (<p:{hh:nat} {dx:nat} add H dx hh -> ho2db x hh (dvar dx)> :: <x:hterm> :: L) (s H) := ctx L H.

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

Abella < Define fresh : lfobj -> lfobj -> prop by 
nabla x, fresh x O.

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

============================
 forall L H, ctx L H -> <H:nat>

ctx_nat < induction on 1.

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

ctx_nat < intros.

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

ctx_nat < case H1.

Subgoal 1:

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

Subgoal 2 is:
 <s H1:nat>

ctx_nat < search.

Subgoal 2:

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

ctx_nat < apply IH to H2.

Subgoal 2:

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

ctx_nat < search.
Proof completed.

Abella < Theorem ctx_inv : 
forall E L H, ctx L H -> member E L -> (exists X, E = <X:hterm> /\ name X) \/
  (exists X P HX, E =
     <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
     <HX:nat> /\ fresh X H /\ le (s HX) H).

============================
 forall E L H, ctx L H -> member E L ->
   (exists X, E = <X:hterm> /\ name X) \/
   (exists X P HX, E =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X H /\ le (s HX) H)

ctx_inv < induction on 1.

IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 forall E L H, ctx L H @ -> member E L ->
   (exists X, E = <X:hterm> /\ name X) \/
   (exists X P HX, E =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X H /\ le (s HX) H)

ctx_inv < intros.

Variables: E L H
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx L H @
H2 : member E L
============================
 (exists X, E = <X:hterm> /\ name X) \/
   (exists X P HX, E =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X H /\ le (s HX) H)

ctx_inv < case H1 (keep).

Subgoal 1:

Variables: E
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx nil z @
H2 : member E nil
============================
 (exists X, E = <X:hterm> /\ name X) \/
   (exists X P HX, E =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X z /\ le (s HX) z)

Subgoal 2 is:
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ 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, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H2 : member (E n1 n2)
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
H3 : ctx L1 H1 *
============================
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ 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, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
============================
 (exists X, <n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> =
    <X:hterm> /\ name X) \/
   (exists X P HX,
      <n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

Subgoal 2.2 is:
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < apply ctx_nat to H3.

Subgoal 2.1:

Variables: H1 L1
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H4 : <H1:nat>
============================
 (exists X, <n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> =
    <X:hterm> /\ name X) \/
   (exists X P HX,
      <n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

Subgoal 2.2 is:
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ 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, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H4 : member (E n1 n2) (<n1:hterm> :: L1)
============================
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < case H4.

Subgoal 2.2.1:

Variables: H1 L1
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
============================
 (exists X, <n1:hterm> = <X:hterm> /\ name X) \/
   (exists X P HX, <n1:hterm> =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

Subgoal 2.2.2 is:
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < left.

Subgoal 2.2.1:

Variables: H1 L1
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
============================
 exists X, <n1:hterm> = <X:hterm> /\ name X

Subgoal 2.2.2 is:
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < search.

Subgoal 2.2.2:

Variables: E H1 L1
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H5 : member (E n1 n2) L1
============================
 (exists X, E n1 n2 = <X:hterm> /\ name X) \/
   (exists X P HX, E n1 n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < apply member_prune to H5.

Subgoal 2.2.2:

Variables: H1 L1 F
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H5 : member (F n2) L1
============================
 (exists X, F n2 = <X:hterm> /\ name X) \/
   (exists X P HX, F n2 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < apply member_prune3 to H5.

Subgoal 2.2.2:

Variables: H1 L1 F1
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H5 : member F1 L1
============================
 (exists X, F1 = <X:hterm> /\ name X) \/
   (exists X P HX, F1 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < apply IH to H3 H5.

Subgoal 2.2.2:

Variables: H1 L1 F1
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H5 : member F1 L1
H6 : (exists X, F1 = <X:hterm> /\ name X) \/
       (exists X P HX, F1 =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H1 /\ le (s HX) H1)
============================
 (exists X, F1 = <X:hterm> /\ name X) \/
   (exists X P HX, F1 =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
      <HX:nat> /\ fresh X (s H1) /\ le (s HX) (s H1))

ctx_inv < case H6.

Subgoal 2.2.2.1:

Variables: H1 L1 X
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H5 : member <X:hterm> L1
H7 : name X
============================
 (exists X1, <X:hterm> = <X1:hterm> /\ name X1) \/
   (exists X1 P HX, <X:hterm> =
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> /\
      <HX:nat> /\ fresh X1 (s H1) /\ le (s HX) (s H1))

Subgoal 2.2.2.2 is:
 (exists X1, <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> =
    <X1:hterm> /\ name X1) \/
   (exists X1 P1 HX1,
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> =
      <P1:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)> /\
      <HX1:nat> /\ fresh X1 (s H1) /\ le (s HX1) (s H1))

ctx_inv < search.

Subgoal 2.2.2.2:

Variables: H1 L1 X P HX
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add H1 dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1)
       (s H1) @
H3 : ctx L1 H1 *
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L1
H7 : <HX:nat>
H8 : fresh X H1
H9 : le (s HX) H1
============================
 (exists X1, <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> =
    <X1:hterm> /\ name X1) \/
   (exists X1 P1 HX1,
      <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> =
      <P1:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)> /\
      <HX1:nat> /\ fresh X1 (s H1) /\ le (s HX1) (s H1))

ctx_inv < case H8.

Subgoal 2.2.2.2:

Variables: L1 P HX O
IH : forall E L H, ctx L H * -> member E L ->
       (exists X, E = <X:hterm> /\ name X) \/
       (exists X P HX, E =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
H1 : ctx
       (<n2:{hh:nat} {dx:nat} add O dx hh -> ho2db n1 hh (dvar dx)> ::
          <n1:hterm> :: L1 n3)
       (s O) @
H3 : ctx (L1 n3) O *
H5 : member
       <P n3:{hh:nat} {dx:nat} add (HX n3) dx hh -> ho2db n3 hh (dvar dx)>
       (L1 n3)
H7 : <HX n3:nat>
H9 : le (s (HX n3)) O
============================
 (exists X1,
    <P n3:{hh:nat} {dx:nat} add (HX n3) dx hh -> ho2db n3 hh (dvar dx)> =
    <X1:hterm> /\ name X1) \/
   (exists X1 P1 HX1,
      <P n3:{hh:nat} {dx:nat} add (HX n3) dx hh -> ho2db n3 hh (dvar dx)> =
      <P1:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)> /\
      <HX1:nat> /\ fresh X1 (s O) /\ le (s HX1) (s O))

ctx_inv < search.
Proof completed.

Abella < Theorem ctx_unique1 : 
forall L H X P1 P2 H1 H2, ctx L H ->
  member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L ->
  member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
  H1 = H2 /\ P1 = P2.

============================
 forall L H X P1 P2 H1 H2, ctx L H ->
   member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L ->
   member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
   H1 = H2 /\ P1 = P2

ctx_unique1 < induction on 2.

IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
============================
 forall L H X P1 P2 H1 H2, ctx L H ->
   member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L @ ->
   member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
   H1 = H2 /\ P1 = P2

ctx_unique1 < intros.

Variables: L H X P1 P2 H1 H2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx L H
H2 : member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L @
H3 : member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L
============================
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H2.

Subgoal 1:

Variables: H X P1 P2 H1 H2 L1
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx (<P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> :: L1)
       H
H3 : member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)>
       (<P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> :: L1)
============================
 H1 = H2 /\ P1 = P2

Subgoal 2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H3.

Subgoal 1.1:

Variables: H X P1 H1 L1
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx (<P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> :: L1)
       H
============================
 H1 = H1 /\ P1 = z1\z2\z3\P1 z1 z2 z3

Subgoal 1.2 is:
 H1 = H2 /\ P1 = P2

Subgoal 2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < search.

Subgoal 1.2:

Variables: H X P1 P2 H1 H2 L1
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx (<P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> :: L1)
       H
H4 : member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L1
============================
 H1 = H2 /\ P1 = P2

Subgoal 2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H1.

Subgoal 1.2:

Variables: P2 H2 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H4 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db n1 hh (dvar dx)>
       (<n1:hterm> :: L2)
H5 : ctx L2 H3
============================
 H3 = H2 n1 n2 /\ z3\z4\z5\n2 z3 z4 z5 = P2 n1 n2

Subgoal 2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H4.

Subgoal 1.2:

Variables: P2 H2 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H5 : ctx L2 H3
H6 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db n1 hh (dvar dx)>
       L2
============================
 H3 = H2 n1 n2 /\ z3\z4\z5\n2 z3 z4 z5 = P2 n1 n2

Subgoal 2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < apply member_prune to H6.

Subgoal 2:

Variables: H X P1 P2 H1 H2 L1 B
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx (B :: L1) H
H3 : member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)>
       (B :: L1)
H4 : member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L1 *
============================
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H3.

Subgoal 2.1:

Variables: H X P1 P2 H1 H2 L1
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx (<P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> :: L1)
       H
H4 : member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L1 *
============================
 H1 = H2 /\ P1 = P2

Subgoal 2.2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H1.

Subgoal 2.1:

Variables: P1 H1 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H4 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (H1 n1 n2) dx hh ->
          ho2db n1 hh (dvar dx)>
       (<n1:hterm> :: L2) *
H5 : ctx L2 H3
============================
 H1 n1 n2 = H3 /\ P1 n1 n2 = z3\z4\z5\n2 z3 z4 z5

Subgoal 2.2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H4.

Subgoal 2.1:

Variables: P1 H1 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H5 : ctx L2 H3
H6 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (H1 n1 n2) dx hh ->
          ho2db n1 hh (dvar dx)>
       L2 *
============================
 H1 n1 n2 = H3 /\ P1 n1 n2 = z3\z4\z5\n2 z3 z4 z5

Subgoal 2.2 is:
 H1 = H2 /\ P1 = P2

ctx_unique1 < apply member_prune to H6.

Subgoal 2.2:

Variables: H X P1 P2 H1 H2 L1 B
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H1 : ctx (B :: L1) H
H4 : member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L1 *
H5 : member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L1
============================
 H1 = H2 /\ P1 = P2

ctx_unique1 < case H1.

Subgoal 2.2:

Variables: X P1 P2 H1 H2 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H4 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (H1 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2) *
H5 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2)
H6 : ctx L2 H3
============================
 H1 n1 n2 = H2 n1 n2 /\ P1 n1 n2 = P2 n1 n2

ctx_unique1 < case H4.

Subgoal 2.2:

Variables: X P1 P2 H1 H2 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H5 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2)
H6 : ctx L2 H3
H7 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (H1 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       L2 *
============================
 H1 n1 n2 = H2 n1 n2 /\ P1 n1 n2 = P2 n1 n2

ctx_unique1 < case H5.

Subgoal 2.2:

Variables: X P1 P2 H1 H2 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H6 : ctx L2 H3
H7 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (H1 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       L2 *
H8 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       L2
============================
 H1 n1 n2 = H2 n1 n2 /\ P1 n1 n2 = P2 n1 n2

ctx_unique1 < apply IH to H6 H7 H8.

Subgoal 2.2:

Variables: X P2 H2 H3 L2
IH : forall L H X P1 P2 H1 H2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add H1 dx hh -> ho2db X hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add H2 dx hh -> ho2db X hh (dvar dx)> L ->
       H1 = H2 /\ P1 = P2
H6 : ctx L2 H3
H7 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       L2 *
H8 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (H2 n1 n2) dx hh ->
          ho2db (X n1 n2) hh (dvar dx)>
       L2
============================
 H2 n1 n2 = H2 n1 n2 /\ z3\z4\z5\P2 n1 n2 z3 z4 z5 = P2 n1 n2

ctx_unique1 < search.
Proof completed.

Abella < Theorem ctx_unique2 : 
forall L H X1 X2 HX P1 P2, ctx L H ->
  member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L ->
  member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
  X1 = X2 /\ P1 = P2.

============================
 forall L H X1 X2 HX P1 P2, ctx L H ->
   member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L ->
   member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
   X1 = X2 /\ P1 = P2

ctx_unique2 < induction on 2.

IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
============================
 forall L H X1 X2 HX P1 P2, ctx L H ->
   member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L @ ->
   member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
   X1 = X2 /\ P1 = P2

ctx_unique2 < intros.

Variables: L H X1 X2 HX P1 P2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx L H
H2 : member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L @
H3 : member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L
============================
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H2.

Subgoal 1:

Variables: H X1 X2 HX P1 P2 L1
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx (<P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> :: L1)
       H
H3 : member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)>
       (<P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> :: L1)
============================
 X1 = X2 /\ P1 = P2

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H3.

Subgoal 1.1:

Variables: H X1 HX P1 L1
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx (<P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> :: L1)
       H
============================
 X1 = X1 /\ P1 = z1\z2\z3\P1 z1 z2 z3

Subgoal 1.2 is:
 X1 = X2 /\ P1 = P2

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < search.

Subgoal 1.2:

Variables: H X1 X2 HX P1 P2 L1
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx (<P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> :: L1)
       H
H4 : member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L1
============================
 X1 = X2 /\ P1 = P2

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H1.

Subgoal 1.2:

Variables: X2 P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H4 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2)
H5 : ctx L2 H1
============================
 n1 = X2 n1 n2 /\ z3\z4\z5\n2 z3 z4 z5 = P2 n1 n2

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H4.

Subgoal 1.2:

Variables: X2 P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : ctx L2 H1
H6 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       L2
============================
 n1 = X2 n1 n2 /\ z3\z4\z5\n2 z3 z4 z5 = P2 n1 n2

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < apply ctx_inv to H5 H6.

Subgoal 1.2:

Variables: X2 P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : ctx L2 H1
H6 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       L2
H7 : (exists X,
        <P2 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
           ho2db (X2 n1 n2) hh (dvar dx)> =
        <X:hterm> /\ name X) \/
       (exists X P HX,
          <P2 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
             ho2db (X2 n1 n2) hh (dvar dx)> =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H1 /\ le (s HX) H1)
============================
 n1 = X2 n1 n2 /\ z3\z4\z5\n2 z3 z4 z5 = P2 n1 n2

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H7.

Subgoal 1.2:

Variables: H1 L2 X P
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : ctx L2 H1
H6 : member
       <P n2 n1:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X n2 n1) hh (dvar dx)>
       L2
H8 : <H1:nat>
H9 : fresh (X n2 n1) H1
H10 : le (s H1) H1
============================
 n1 = X n2 n1 /\ z3\z4\z5\n2 z3 z4 z5 = z3\z4\z5\P n2 n1 z3 z4 z5

Subgoal 2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < apply le_absurd to _ H10.

Subgoal 2:

Variables: H X1 X2 HX P1 P2 L1 B
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx (B :: L1) H
H3 : member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)>
       (B :: L1)
H4 : member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L1 *
============================
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H3.

Subgoal 2.1:

Variables: H X1 X2 HX P1 P2 L1
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx (<P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> :: L1)
       H
H4 : member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L1 *
============================
 X1 = X2 /\ P1 = P2

Subgoal 2.2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H1.

Subgoal 2.1:

Variables: X1 P1 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H4 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X1 n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2) *
H5 : ctx L2 H1
============================
 X1 n1 n2 = n1 /\ P1 n1 n2 = z3\z4\z5\n2 z3 z4 z5

Subgoal 2.2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H4.

Subgoal 2.1:

Variables: X1 P1 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : ctx L2 H1
H6 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X1 n1 n2) hh (dvar dx)>
       L2 *
============================
 X1 n1 n2 = n1 /\ P1 n1 n2 = z3\z4\z5\n2 z3 z4 z5

Subgoal 2.2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < apply ctx_inv to H5 H6.

Subgoal 2.1:

Variables: X1 P1 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : ctx L2 H1
H6 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X1 n1 n2) hh (dvar dx)>
       L2 *
H7 : (exists X,
        <P1 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
           ho2db (X1 n1 n2) hh (dvar dx)> =
        <X:hterm> /\ name X) \/
       (exists X P HX,
          <P1 n1 n2:{hh:nat} {dx:nat} add H1 dx hh ->
             ho2db (X1 n1 n2) hh (dvar dx)> =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H1 /\ le (s HX) H1)
============================
 X1 n1 n2 = n1 /\ P1 n1 n2 = z3\z4\z5\n2 z3 z4 z5

Subgoal 2.2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H7.

Subgoal 2.1:

Variables: H1 L2 X P
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : ctx L2 H1
H6 : member
       <P n2 n1:{hh:nat} {dx:nat} add H1 dx hh ->
          ho2db (X n2 n1) hh (dvar dx)>
       L2 *
H8 : <H1:nat>
H9 : fresh (X n2 n1) H1
H10 : le (s H1) H1
============================
 X n2 n1 = n1 /\ z3\z4\z5\P n2 n1 z3 z4 z5 = z3\z4\z5\n2 z3 z4 z5

Subgoal 2.2 is:
 X1 = X2 /\ P1 = P2

ctx_unique2 < apply le_absurd to _ H10.

Subgoal 2.2:

Variables: H X1 X2 HX P1 P2 L1 B
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H1 : ctx (B :: L1) H
H4 : member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L1 *
H5 : member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L1
============================
 X1 = X2 /\ P1 = P2

ctx_unique2 < case H1.

Subgoal 2.2:

Variables: X1 X2 HX P1 P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H4 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X1 n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2) *
H5 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2)
H6 : ctx L2 H1
============================
 X1 n1 n2 = X2 n1 n2 /\ P1 n1 n2 = P2 n1 n2

ctx_unique2 < case H4.

Subgoal 2.2:

Variables: X1 X2 HX P1 P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H5 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       (<n1:hterm> :: L2)
H6 : ctx L2 H1
H7 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X1 n1 n2) hh (dvar dx)>
       L2 *
============================
 X1 n1 n2 = X2 n1 n2 /\ P1 n1 n2 = P2 n1 n2

ctx_unique2 < case H5.

Subgoal 2.2:

Variables: X1 X2 HX P1 P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H6 : ctx L2 H1
H7 : member
       <P1 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X1 n1 n2) hh (dvar dx)>
       L2 *
H8 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       L2
============================
 X1 n1 n2 = X2 n1 n2 /\ P1 n1 n2 = P2 n1 n2

ctx_unique2 < apply IH to _ H7 H8.

Subgoal 2.2:

Variables: X2 HX P2 H1 L2
IH : forall L H X1 X2 HX P1 P2, ctx L H ->
       member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X1 hh (dvar dx)> L * ->
       member <P2:{hh:nat} {dx:nat} add HX dx hh -> ho2db X2 hh (dvar dx)> L ->
       X1 = X2 /\ P1 = P2
H6 : ctx L2 H1
H7 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       L2 *
H8 : member
       <P2 n1 n2:{hh:nat} {dx:nat} add (HX n1 n2) dx hh ->
          ho2db (X2 n1 n2) hh (dvar dx)>
       L2
============================
 X2 n1 n2 = X2 n1 n2 /\ z3\z4\z5\P2 n1 n2 z3 z4 z5 = P2 n1 n2

ctx_unique2 < search.
Proof completed.

Abella < Theorem nat_ignores_ctx : 
forall L H N, ctx L H -> <L |- N:nat> -> <N:nat>.

============================
 forall L H N, ctx L H -> <L |- N:nat> -> <N:nat>

nat_ignores_ctx < induction on 2.

IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
============================
 forall L H N, ctx L H -> <L |- N:nat>@ -> <N:nat>

nat_ignores_ctx < intros.

Variables: L H N
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H2 : <L |- N:nat>@
============================
 <N:nat>

nat_ignores_ctx < case H2.

Subgoal 1:

Variables: L H
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
============================
 <z:nat>

Subgoal 2 is:
 <s lf_1:nat>

Subgoal 3 is:
 <N:nat>

nat_ignores_ctx < search.

Subgoal 2:

Variables: L H lf_1
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H3 : <L |- lf_1:nat>*
============================
 <s lf_1:nat>

Subgoal 3 is:
 <N:nat>

nat_ignores_ctx < apply IH to H1 H3.

Subgoal 2:

Variables: L H lf_1
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H3 : <L |- lf_1:nat>*
H4 : <lf_1:nat>
============================
 <s lf_1:nat>

Subgoal 3 is:
 <N:nat>

nat_ignores_ctx < search.

Subgoal 3:

Variables: L H N F
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H3 : <L, [F] |- N:nat>*
H4 : member F L
============================
 <N:nat>

nat_ignores_ctx < apply ctx_inv to H1 H4.

Subgoal 3:

Variables: L H N F
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H3 : <L, [F] |- N:nat>*
H4 : member F L
H5 : (exists X, F = <X:hterm> /\ name X) \/
       (exists X P HX, F =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 <N:nat>

nat_ignores_ctx < case H5.

Subgoal 3.1:

Variables: L H N X
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H3 : <L, [X:hterm] |- N:nat>*
H4 : member <X:hterm> L
H6 : name X
============================
 <N:nat>

Subgoal 3.2 is:
 <N:nat>

nat_ignores_ctx < case H3.

Subgoal 3.2:

Variables: L H N X P HX
IH : forall L H N, ctx L H -> <L |- N:nat>* -> <N:nat>
H1 : ctx L H
H3 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- N:nat>*
H4 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H6 : <HX:nat>
H7 : fresh X H
H8 : le (s HX) H
============================
 <N:nat>

nat_ignores_ctx < case H3.
Proof completed.

Abella < Theorem add_ignores_ctx : 
forall L H A B C P, ctx L H -> <L |- P:add A B C> ->
  (exists Q, <Q:add A B C>).

============================
 forall L H A B C P, ctx L H -> <L |- P:add A B C> ->
   (exists Q, <Q:add A B C>)

add_ignores_ctx < induction on 2.

IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
============================
 forall L H A B C P, ctx L H -> <L |- P:add A B C>@ ->
   (exists Q, <Q:add A B C>)

add_ignores_ctx < intros.

Variables: L H A B C P
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H2 : <L |- P:add A B C>@
============================
 exists Q, <Q:add A B C>

add_ignores_ctx < case H2.

Subgoal 1:

Variables: L H C
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- C:nat>*
============================
 exists Q, <Q:add z C C>

Subgoal 2 is:
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < apply nat_ignores_ctx to H1 H3.

Subgoal 1:

Variables: L H C
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- C:nat>*
H4 : <C:nat>
============================
 exists Q, <Q:add z C C>

Subgoal 2 is:
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < search.

Subgoal 2:

Variables: L H B C1 A1 lf_1
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- A1:nat>*
H4 : <L |- B:nat>*
H5 : <L |- C1:nat>*
H6 : <L |- lf_1:add A1 B C1>*
============================
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < apply IH to H1 H6.

Subgoal 2:

Variables: L H B C1 A1 lf_1 Q
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- A1:nat>*
H4 : <L |- B:nat>*
H5 : <L |- C1:nat>*
H6 : <L |- lf_1:add A1 B C1>*
H7 : <Q:add A1 B C1>
============================
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < apply nat_ignores_ctx to _ H3.

Subgoal 2:

Variables: L H B C1 A1 lf_1 Q
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- A1:nat>*
H4 : <L |- B:nat>*
H5 : <L |- C1:nat>*
H6 : <L |- lf_1:add A1 B C1>*
H7 : <Q:add A1 B C1>
H8 : <A1:nat>
============================
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < apply nat_ignores_ctx to _ H4.

Subgoal 2:

Variables: L H B C1 A1 lf_1 Q
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- A1:nat>*
H4 : <L |- B:nat>*
H5 : <L |- C1:nat>*
H6 : <L |- lf_1:add A1 B C1>*
H7 : <Q:add A1 B C1>
H8 : <A1:nat>
H9 : <B:nat>
============================
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < apply nat_ignores_ctx to _ H5.

Subgoal 2:

Variables: L H B C1 A1 lf_1 Q
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L |- A1:nat>*
H4 : <L |- B:nat>*
H5 : <L |- C1:nat>*
H6 : <L |- lf_1:add A1 B C1>*
H7 : <Q:add A1 B C1>
H8 : <A1:nat>
H9 : <B:nat>
H10 : <C1:nat>
============================
 exists Q, <Q:add (s A1) B (s C1)>

Subgoal 3 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < search.

Subgoal 3:

Variables: L H A B C P F
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L, [F] |- P:add A B C>*
H4 : member F L
============================
 exists Q, <Q:add A B C>

add_ignores_ctx < apply ctx_inv to H1 H4.

Subgoal 3:

Variables: L H A B C P F
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L, [F] |- P:add A B C>*
H4 : member F L
H5 : (exists X, F = <X:hterm> /\ name X) \/
       (exists X P HX, F =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 exists Q, <Q:add A B C>

add_ignores_ctx < case H5.

Subgoal 3.1:

Variables: L H A B C P X
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L, [X:hterm] |- P:add A B C>*
H4 : member <X:hterm> L
H6 : name X
============================
 exists Q, <Q:add A B C>

Subgoal 3.2 is:
 exists Q, <Q:add A B C>

add_ignores_ctx < case H3.

Subgoal 3.2:

Variables: L H A B C P X P1 HX
IH : forall L H A B C P, ctx L H -> <L |- P:add A B C>* ->
       (exists Q, <Q:add A B C>)
H1 : ctx L H
H3 : <L, [P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P:
        add A B C>*
H4 : member <P1:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H6 : <HX:nat>
H7 : fresh X H
H8 : le (s HX) H
============================
 exists Q, <Q:add A B C>

add_ignores_ctx < case H3.
Proof completed.

Abella < Theorem ho2db_det3 : 
forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1> ->
  <L |- P2:ho2db M H D2> -> D1 = D2.

============================
 forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1> ->
   <L |- P2:ho2db M H D2> -> D1 = D2

ho2db_det3 < induction on 2.

IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
============================
 forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>@ ->
   <L |- P2:ho2db M H D2> -> D1 = D2

ho2db_det3 < intros.

Variables: L M D1 D2 H P1 P2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H2 : <L |- P1:ho2db M H D1>@
H3 : <L |- P2:ho2db M H D2>
============================
 D1 = D2

ho2db_det3 < case H2.

Subgoal 1:

Variables: L D2 H P2 DN N lf_2 DM M1 lf_1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db (happ M1 N) H D2>
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM>*
H10 : <L |- lf_2: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 lf_2 DM M1 lf_1 DN1 lf_4 DM1 lf_3
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L |- M1:hterm>
H12 : <L |- N:hterm>
H13 : <L |- H:nat>
H14 : <L |- DM1:dterm>
H15 : <L |- DN1:dterm>
H16 : <L |- lf_3:ho2db M1 H DM1>
H17 : <L |- lf_4: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 _ H9 H16.

Subgoal 1.1:

Variables: L H DN N lf_2 M1 lf_1 DN1 lf_4 DM1 lf_3
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM1:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM1>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L |- M1:hterm>
H12 : <L |- N:hterm>
H13 : <L |- H:nat>
H14 : <L |- DM1:dterm>
H15 : <L |- DN1:dterm>
H16 : <L |- lf_3:ho2db M1 H DM1>
H17 : <L |- lf_4: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 _ H10 H17.

Subgoal 1.1:

Variables: L H N lf_2 M1 lf_1 DN1 lf_4 DM1 lf_3
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM1:dterm>*
H8 : <L |- DN1:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM1>*
H10 : <L |- lf_2:ho2db N H DN1>*
H11 : <L |- M1:hterm>
H12 : <L |- N:hterm>
H13 : <L |- H:nat>
H14 : <L |- DM1:dterm>
H15 : <L |- DN1:dterm>
H16 : <L |- lf_3:ho2db M1 H DM1>
H17 : <L |- lf_4: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 P2 DN N lf_2 DM M1 lf_1 F
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [F] |- P2:ho2db (happ M1 N) H D2>
H12 : 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 H12.

Subgoal 1.2:

Variables: L D2 H P2 DN N lf_2 DM M1 lf_1 F
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [F] |- P2:ho2db (happ M1 N) H D2>
H12 : member F L
H13 : (exists X, F = <X:hterm> /\ name X) \/
        (exists X P HX, F =
           <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
           <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 dapp DM DN = D2

Subgoal 2 is:
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H13.

Subgoal 1.2.1:

Variables: L D2 H P2 DN N lf_2 DM M1 lf_1 X
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [X:hterm] |- P2:ho2db (happ M1 N) H D2>
H12 : member <X:hterm> L
H14 : name X
============================
 dapp DM DN = D2

Subgoal 1.2.2 is:
 dapp DM DN = D2

Subgoal 2 is:
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H11.

Subgoal 1.2.2:

Variables: L D2 H P2 DN N lf_2 DM M1 lf_1 X P HX
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L |- M1:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M1 H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P2:
         ho2db (happ M1 N) H D2>
H12 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H14 : <HX:nat>
H15 : fresh X H
H16 : le (s HX) H
============================
 dapp DM DN = D2

Subgoal 2 is:
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H15.

Subgoal 1.2.2:

Variables: L D2 P2 DN N lf_2 DM M1 lf_1 P HX O
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx (L n1) O
H4 : <L n1 |- M1 n1:hterm>*
H5 : <L n1 |- N n1:hterm>*
H6 : <L n1 |- O:nat>*
H7 : <L n1 |- DM n1:dterm>*
H8 : <L n1 |- DN n1:dterm>*
H9 : <L n1 |- lf_1 n1:ho2db (M1 n1) O (DM n1)>*
H10 : <L n1 |- lf_2 n1:ho2db (N n1) O (DN n1)>*
H11 : <L n1,
         [P n1:{hh:nat} {dx:nat} add (HX n1) dx hh -> ho2db n1 hh (dvar dx)] |-
         P2 n1:ho2db (happ (M1 n1) (N n1)) O (D2 n1)>
H12 : member
        <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H14 : <HX n1:nat>
H16 : le (s (HX n1)) O
============================
 dapp (DM n1) (DN n1) = D2 n1

Subgoal 2 is:
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H11.

Subgoal 2:

Variables: L D2 H P2 DR R lf_1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db (hlam R) H D2>
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2: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 lf_1 DR1 lf_2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, n1:hterm |- R n1:hterm>
H9 : <L |- H:nat>
H10 : <L |- DR1:dterm>
H11 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
         lf_2 n1 n2: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 _ H7 H11.

Subgoal 2.1:

Variables: L H R lf_1 DR1 lf_2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR1:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR1>*
H8 : <L, n1:hterm |- R n1:hterm>
H9 : <L |- H:nat>
H10 : <L |- DR1:dterm>
H11 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
         lf_2 n1 n2: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 P2 DR R lf_1 F
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [F] |- P2:ho2db (hlam R) H D2>
H9 : member F L
============================
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < apply ctx_inv to H1 H9.

Subgoal 2.2:

Variables: L D2 H P2 DR R lf_1 F
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [F] |- P2:ho2db (hlam R) H D2>
H9 : member F L
H10 : (exists X, F = <X:hterm> /\ name X) \/
        (exists X P HX, F =
           <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
           <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H10.

Subgoal 2.2.1:

Variables: L D2 H P2 DR R lf_1 X
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [X:hterm] |- P2:ho2db (hlam R) H D2>
H9 : member <X:hterm> L
H11 : name X
============================
 dlam DR = D2

Subgoal 2.2.2 is:
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H8.

Subgoal 2.2.2:

Variables: L D2 H P2 DR R lf_1 X P HX
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P2:
        ho2db (hlam R) H D2>
H9 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H11 : <HX:nat>
H12 : fresh X H
H13 : le (s HX) H
============================
 dlam DR = D2

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H12.

Subgoal 2.2.2:

Variables: L D2 P2 DR R lf_1 P HX O
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx (L n3) O
H4 : <L n3, n1:hterm |- R n3 n1:hterm>*
H5 : <L n3 |- O:nat>*
H6 : <L n3 |- DR n3:dterm>*
H7 : <L n3, n1:hterm,
      n2:{hh:nat} {dx:nat} add O dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n3 n1 n2:ho2db (R n3 n1) (s O) (DR n3)>*
H8 : <L n3,
        [P n3:{hh:nat} {dx:nat} add (HX n3) dx hh -> ho2db n3 hh (dvar dx)] |-
        P2 n3:ho2db (hlam (R n3)) O (D2 n3)>
H9 : member
       <P n3:{hh:nat} {dx:nat} add (HX n3) dx hh -> ho2db n3 hh (dvar dx)>
       (L n3)
H11 : <HX n3:nat>
H13 : le (s (HX n3)) O
============================
 dlam (DR n3) = D2 n3

Subgoal 3 is:
 D1 = D2

ho2db_det3 < case H8.

Subgoal 3:

Variables: L M D1 D2 H P1 P2 F
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db M H D2>
H4 : <L, [F] |- P1: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 P1 P2 F
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db M H D2>
H4 : <L, [F] |- P1:ho2db M H D1>*
H5 : member F L
H6 : (exists X, F = <X:hterm> /\ name X) \/
       (exists X P HX, F =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 D1 = D2

ho2db_det3 < case H6.

Subgoal 3.1:

Variables: L M D1 D2 H P1 P2 X
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db M H D2>
H4 : <L, [X:hterm] |- P1:ho2db M H D1>*
H5 : member <X:hterm> L
H7 : name X
============================
 D1 = D2

Subgoal 3.2 is:
 D1 = D2

ho2db_det3 < case H4.

Subgoal 3.2:

Variables: L M D1 D2 H P1 P2 X P HX
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db M H D2>
H4 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P1:
        ho2db M H D1>*
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh X H
H9 : le (s HX) H
============================
 D1 = D2

ho2db_det3 < case H4.

Subgoal 3.2:

Variables: L M D2 H P2 P HX dx lf_1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H3 : <L |- P2:ho2db M H D2>
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
============================
 dvar dx = D2

ho2db_det3 < case H3.

Subgoal 3.2.1:

Variables: L H P HX dx lf_1 DN N lf_3 DM M1 lf_2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member
       <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db (happ M1 N) hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh (happ M1 N) H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L |- M1:hterm>
H14 : <L |- N:hterm>
H15 : <L |- H:nat>
H16 : <L |- DM:dterm>
H17 : <L |- DN:dterm>
H18 : <L |- lf_2:ho2db M1 H DM>
H19 : <L |- lf_3:ho2db N H DN>
============================
 dvar dx = dapp DM DN

Subgoal 3.2.2 is:
 dvar dx = dlam DR

Subgoal 3.2.3 is:
 dvar dx = D2

ho2db_det3 < case H8.

Subgoal 3.2.2:

Variables: L H P HX dx lf_1 DR R lf_2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db (hlam R) hh (dvar dx)>
       L
H7 : <HX:nat>
H8 : fresh (hlam R) H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, n1:hterm |- R n1:hterm>
H14 : <L |- H:nat>
H15 : <L |- DR:dterm>
H16 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
         lf_2 n1 n2:ho2db (R n1) (s H) DR>
============================
 dvar dx = dlam DR

Subgoal 3.2.3 is:
 dvar dx = D2

ho2db_det3 < case H8.

Subgoal 3.2.3:

Variables: L M D2 H P2 P HX dx lf_1 F1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [F1] |- P2:ho2db M H D2>
H14 : member F1 L
============================
 dvar dx = D2

ho2db_det3 < apply ctx_inv to H1 H14.

Subgoal 3.2.3:

Variables: L M D2 H P2 P HX dx lf_1 F1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [F1] |- P2:ho2db M H D2>
H14 : member F1 L
H15 : (exists X, F1 = <X:hterm> /\ name X) \/
        (exists X P HX, F1 =
           <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
           <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 dvar dx = D2

ho2db_det3 < case H15.

Subgoal 3.2.3.1:

Variables: L M D2 H P2 P HX dx lf_1 X1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [X1:hterm] |- P2:ho2db M H D2>
H14 : member <X1:hterm> L
H16 : name X1
============================
 dvar dx = D2

Subgoal 3.2.3.2 is:
 dvar dx = D2

ho2db_det3 < case H13.

Subgoal 3.2.3.2:

Variables: L M D2 H P2 P HX dx lf_1 X1 P3 HX1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)] |-
         P2:ho2db M H D2>
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh X1 H
H18 : le (s HX1) H
============================
 dvar dx = D2

ho2db_det3 < case H13.

Subgoal 3.2.3.2:

Variables: L M H P HX dx lf_1 P3 HX1 dx1 lf_2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
============================
 dvar dx = dvar dx1

ho2db_det3 < apply ctx_unique1 to H1 H5 H14.

Subgoal 3.2.3.2:

Variables: L M H dx lf_1 P3 HX1 dx1 lf_2
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX1 dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
============================
 dvar dx = dvar dx1

ho2db_det3 < apply add_ignores_ctx to _ H12.

Subgoal 3.2.3.2:

Variables: L M H dx lf_1 P3 HX1 dx1 lf_2 Q
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX1 dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
H22 : <Q:add HX1 dx H>
============================
 dvar dx = dvar dx1

ho2db_det3 < apply add_ignores_ctx to _ H21.

Subgoal 3.2.3.2:

Variables: L M H dx lf_1 P3 HX1 dx1 lf_2 Q Q1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX1 dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
H22 : <Q:add HX1 dx H>
H23 : <Q1:add HX1 dx1 H>
============================
 dvar dx = dvar dx1

ho2db_det3 < apply add_det2 to _ _ _ _ H22 H23.

Subgoal 3.2.3.2.1:

Variables: L M H dx lf_1 P3 HX1 dx1 lf_2 Q Q1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX1 dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
H22 : <Q:add HX1 dx H>
H23 : <Q1:add HX1 dx1 H>
============================
 <H:nat>

Subgoal 3.2.3.2.2 is:
 <dx1:nat>

Subgoal 3.2.3.2.3 is:
 <dx:nat>

Subgoal 3.2.3.2 is:
 dvar dx1 = dvar dx1

ho2db_det3 < backchain nat_ignores_ctx.

Subgoal 3.2.3.2.2:

Variables: L M H dx lf_1 P3 HX1 dx1 lf_2 Q Q1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX1 dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
H22 : <Q:add HX1 dx H>
H23 : <Q1:add HX1 dx1 H>
============================
 <dx1:nat>

Subgoal 3.2.3.2.3 is:
 <dx:nat>

Subgoal 3.2.3.2 is:
 dvar dx1 = dvar dx1

ho2db_det3 < backchain nat_ignores_ctx.

Subgoal 3.2.3.2.3:

Variables: L M H dx lf_1 P3 HX1 dx1 lf_2 Q Q1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX1 dx H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
H22 : <Q:add HX1 dx H>
H23 : <Q1:add HX1 dx1 H>
============================
 <dx:nat>

Subgoal 3.2.3.2 is:
 dvar dx1 = dvar dx1

ho2db_det3 < backchain nat_ignores_ctx.

Subgoal 3.2.3.2:

Variables: L M H lf_1 P3 HX1 dx1 lf_2 Q Q1
IH : forall L M D1 D2 H P1 P2, ctx L H -> <L |- P1:ho2db M H D1>* ->
       <L |- P2:ho2db M H D2> -> D1 = D2
H1 : ctx L H
H5 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H7 : <HX1:nat>
H8 : fresh M H
H9 : le (s HX1) H
H10 : <L |- H:nat>*
H11 : <L |- dx1:nat>*
H12 : <L |- lf_1:add HX1 dx1 H>*
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db M hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh M H
H18 : le (s HX1) H
H19 : <L |- H:nat>
H20 : <L |- dx1:nat>
H21 : <L |- lf_2:add HX1 dx1 H>
H22 : <Q:add HX1 dx1 H>
H23 : <Q1:add HX1 dx1 H>
============================
 dvar dx1 = dvar dx1

ho2db_det3 < search.
Proof completed.

Abella < Theorem ho2db_det3_simple : 
forall M D1 D2 P1 P2, <P1:ho2db M z D1> -> <P2:ho2db M z D2> -> D1 = D2.

============================
 forall M D1 D2 P1 P2, <P1:ho2db M z D1> -> <P2:ho2db M z D2> -> D1 = D2

ho2db_det3_simple < intros.

Variables: M D1 D2 P1 P2
H1 : <P1:ho2db M z D1>
H2 : <P2:ho2db M z D2>
============================
 D1 = D2

ho2db_det3_simple < apply ho2db_det3 to _ H1 H2.

Variables: M D2 P1 P2
H1 : <P1:ho2db M z D2>
H2 : <P2:ho2db M z D2>
============================
 D2 = D2

ho2db_det3_simple < search.
Proof completed.

Abella < Theorem ho2db_det1 : 
forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D> ->
  <L |- P2:ho2db M2 H D> -> M1 = M2.

============================
 forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D> ->
   <L |- P2:ho2db M2 H D> -> M1 = M2

ho2db_det1 < induction on 2.

IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
============================
 forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>@ ->
   <L |- P2:ho2db M2 H D> -> M1 = M2

ho2db_det1 < intros.

Variables: L M1 M2 D H P1 P2
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H2 : <L |- P1:ho2db M1 H D>@
H3 : <L |- P2:ho2db M2 H D>
============================
 M1 = M2

ho2db_det1 < case H2.

Subgoal 1:

Variables: L M2 H P2 DN N lf_2 DM M lf_1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H3 : <L |- P2:ho2db M2 H (dapp DM DN)>
H4 : <L |- M:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
============================
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H3.

Subgoal 1.1:

Variables: L H DN N lf_2 DM M lf_1 N1 lf_4 M3 lf_3
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L |- M3:hterm>
H12 : <L |- N1:hterm>
H13 : <L |- H:nat>
H14 : <L |- DM:dterm>
H15 : <L |- DN:dterm>
H16 : <L |- lf_3:ho2db M3 H DM>
H17 : <L |- lf_4:ho2db N1 H DN>
============================
 happ M N = happ M3 N1

Subgoal 1.2 is:
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < apply IH to _ H9 H16.

Subgoal 1.1:

Variables: L H DN N lf_2 DM lf_1 N1 lf_4 M3 lf_3
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M3:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M3 H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L |- M3:hterm>
H12 : <L |- N1:hterm>
H13 : <L |- H:nat>
H14 : <L |- DM:dterm>
H15 : <L |- DN:dterm>
H16 : <L |- lf_3:ho2db M3 H DM>
H17 : <L |- lf_4:ho2db N1 H DN>
============================
 happ M3 N = happ M3 N1

Subgoal 1.2 is:
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < apply IH to _ H10 H17.

Subgoal 1.1:

Variables: L H DN lf_2 DM lf_1 N1 lf_4 M3 lf_3
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M3:hterm>*
H5 : <L |- N1:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M3 H DM>*
H10 : <L |- lf_2:ho2db N1 H DN>*
H11 : <L |- M3:hterm>
H12 : <L |- N1:hterm>
H13 : <L |- H:nat>
H14 : <L |- DM:dterm>
H15 : <L |- DN:dterm>
H16 : <L |- lf_3:ho2db M3 H DM>
H17 : <L |- lf_4:ho2db N1 H DN>
============================
 happ M3 N1 = happ M3 N1

Subgoal 1.2 is:
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < search.

Subgoal 1.2:

Variables: L M2 H P2 DN N lf_2 DM M lf_1 F
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [F] |- P2:ho2db M2 H (dapp DM DN)>
H12 : member F L
============================
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < apply ctx_inv to _ H12.

Subgoal 1.2:

Variables: L M2 H P2 DN N lf_2 DM M lf_1 F
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [F] |- P2:ho2db M2 H (dapp DM DN)>
H12 : member F L
H13 : (exists X, F = <X:hterm> /\ name X) \/
        (exists X P HX, F =
           <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
           <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H13.

Subgoal 1.2.1:

Variables: L M2 H P2 DN N lf_2 DM M lf_1 X
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [X:hterm] |- P2:ho2db M2 H (dapp DM DN)>
H12 : member <X:hterm> L
H14 : name X
============================
 happ M N = M2

Subgoal 1.2.2 is:
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H11.

Subgoal 1.2.2:

Variables: L M2 H P2 DN N lf_2 DM M lf_1 X P HX
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L |- M:hterm>*
H5 : <L |- N:hterm>*
H6 : <L |- H:nat>*
H7 : <L |- DM:dterm>*
H8 : <L |- DN:dterm>*
H9 : <L |- lf_1:ho2db M H DM>*
H10 : <L |- lf_2:ho2db N H DN>*
H11 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P2:
         ho2db M2 H (dapp DM DN)>
H12 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H14 : <HX:nat>
H15 : fresh X H
H16 : le (s HX) H
============================
 happ M N = M2

Subgoal 2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H11.

Subgoal 2:

Variables: L M2 H P2 DR R lf_1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H3 : <L |- P2:ho2db M2 H (dlam DR)>
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
============================
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H3.

Subgoal 2.1:

Variables: L H DR R lf_1 R1 lf_2
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, n1:hterm |- R1 n1:hterm>
H9 : <L |- H:nat>
H10 : <L |- DR:dterm>
H11 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
         lf_2 n1 n2:ho2db (R1 n1) (s H) DR>
============================
 hlam R = hlam R1

Subgoal 2.2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < apply IH to _ H7 H11.

Subgoal 2.1:

Variables: L H DR lf_1 R1 lf_2
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L, n1:hterm |- R1 n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R1 n1) (s H) DR>*
H8 : <L, n1:hterm |- R1 n1:hterm>
H9 : <L |- H:nat>
H10 : <L |- DR:dterm>
H11 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
         lf_2 n1 n2:ho2db (R1 n1) (s H) DR>
============================
 hlam (z1\R1 z1) = hlam R1

Subgoal 2.2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < search.

Subgoal 2.2:

Variables: L M2 H P2 DR R lf_1 F
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [F] |- P2:ho2db M2 H (dlam DR)>
H9 : member F L
============================
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < apply ctx_inv to _ H9.

Subgoal 2.2:

Variables: L M2 H P2 DR R lf_1 F
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [F] |- P2:ho2db M2 H (dlam DR)>
H9 : member F L
H10 : (exists X, F = <X:hterm> /\ name X) \/
        (exists X P HX, F =
           <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
           <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H10.

Subgoal 2.2.1:

Variables: L M2 H P2 DR R lf_1 X
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [X:hterm] |- P2:ho2db M2 H (dlam DR)>
H9 : member <X:hterm> L
H11 : name X
============================
 hlam R = M2

Subgoal 2.2.2 is:
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H8.

Subgoal 2.2.2:

Variables: L M2 H P2 DR R lf_1 X P HX
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H4 : <L, n1:hterm |- R n1:hterm>*
H5 : <L |- H:nat>*
H6 : <L |- DR:dterm>*
H7 : <L, n1:hterm, n2:{hh:nat} {dx:nat} add H dx hh -> ho2db n1 hh (dvar dx) |-
        lf_1 n1 n2:ho2db (R n1) (s H) DR>*
H8 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P2:
        ho2db M2 H (dlam DR)>
H9 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H11 : <HX:nat>
H12 : fresh X H
H13 : le (s HX) H
============================
 hlam R = M2

Subgoal 3 is:
 M1 = M2

ho2db_det1 < case H8.

Subgoal 3:

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

ho2db_det1 < apply ctx_inv to _ H5.

Subgoal 3:

Variables: L M1 M2 D H P1 P2 F
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H3 : <L |- P2:ho2db M2 H D>
H4 : <L, [F] |- P1:ho2db M1 H D>*
H5 : member F L
H6 : (exists X, F = <X:hterm> /\ name X) \/
       (exists X P HX, F =
          <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
          <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 M1 = M2

ho2db_det1 < case H6.

Subgoal 3.1:

Variables: L M1 M2 D H P1 P2 X
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H3 : <L |- P2:ho2db M2 H D>
H4 : <L, [X:hterm] |- P1:ho2db M1 H D>*
H5 : member <X:hterm> L
H7 : name X
============================
 M1 = M2

Subgoal 3.2 is:
 M1 = M2

ho2db_det1 < case H4.

Subgoal 3.2:

Variables: L M1 M2 D H P1 P2 X P HX
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H3 : <L |- P2:ho2db M2 H D>
H4 : <L, [P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)] |- P1:
        ho2db M1 H D>*
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh X H
H9 : le (s HX) H
============================
 M1 = M2

ho2db_det1 < case H4.

Subgoal 3.2:

Variables: L M1 M2 H P2 P HX dx lf_1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H3 : <L |- P2:ho2db M2 H (dvar dx)>
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M1 hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M1 H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
============================
 M1 = M2

ho2db_det1 < case H3.

Subgoal 3.2:

Variables: L M1 M2 H P2 P HX dx lf_1 F1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M1 hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M1 H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [F1] |- P2:ho2db M2 H (dvar dx)>
H14 : member F1 L
============================
 M1 = M2

ho2db_det1 < apply ctx_inv to _ H14.

Subgoal 3.2:

Variables: L M1 M2 H P2 P HX dx lf_1 F1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M1 hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M1 H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [F1] |- P2:ho2db M2 H (dvar dx)>
H14 : member F1 L
H15 : (exists X, F1 = <X:hterm> /\ name X) \/
        (exists X P HX, F1 =
           <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db X hh (dvar dx)> /\
           <HX:nat> /\ fresh X H /\ le (s HX) H)
============================
 M1 = M2

ho2db_det1 < case H15.

Subgoal 3.2.1:

Variables: L M1 M2 H P2 P HX dx lf_1 X1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M1 hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M1 H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [X1:hterm] |- P2:ho2db M2 H (dvar dx)>
H14 : member <X1:hterm> L
H16 : name X1
============================
 M1 = M2

Subgoal 3.2.2 is:
 M1 = M2

ho2db_det1 < case H13.

Subgoal 3.2.2:

Variables: L M1 M2 H P2 P HX dx lf_1 X1 P3 HX1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx L H
H5 : member <P:{hh:nat} {dx:nat} add HX dx hh -> ho2db M1 hh (dvar dx)> L
H7 : <HX:nat>
H8 : fresh M1 H
H9 : le (s HX) H
H10 : <L |- H:nat>*
H11 : <L |- dx:nat>*
H12 : <L |- lf_1:add HX dx H>*
H13 : <L, [P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)] |-
         P2:ho2db M2 H (dvar dx)>
H14 : member <P3:{hh:nat} {dx:nat} add HX1 dx hh -> ho2db X1 hh (dvar dx)> L
H16 : <HX1:nat>
H17 : fresh X1 H
H18 : le (s HX1) H
============================
 M1 = M2

ho2db_det1 < case H17.

Subgoal 3.2.2:

Variables: L M1 M2 P2 P HX dx lf_1 P3 HX1 O
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX n1) (dx n1) O>*
H13 : <L n1,
         [P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh ->
            ho2db n1 hh (dvar dx)] |-
         P2 n1:ho2db (M2 n1) O (dvar (dx n1))>
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
============================
 M1 n1 = M2 n1

ho2db_det1 < case H13.

Subgoal 3.2.2:

Variables: L M1 P HX dx lf_1 P3 HX1 O lf_2
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
============================
 M1 n1 = n1

ho2db_det1 < apply ctx_nat to H1.

Subgoal 3.2.2:

Variables: L M1 P HX dx lf_1 P3 HX1 O lf_2
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
H22 : <O:nat>
============================
 M1 n1 = n1

ho2db_det1 < apply add_ignores_ctx to _ H12.

Subgoal 3.2.2:

Variables: L M1 P HX dx lf_1 P3 HX1 O lf_2 Q
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
H22 : <O:nat>
H23 : <Q n1:add (HX n1) (dx n1) O>
============================
 M1 n1 = n1

ho2db_det1 < apply add_ignores_ctx to _ H21.

Subgoal 3.2.2:

Variables: L M1 P HX dx lf_1 P3 HX1 O lf_2 Q Q1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
H22 : <O:nat>
H23 : <Q n1:add (HX n1) (dx n1) O>
H24 : <Q1 n1:add (HX1 n1) (dx n1) O>
============================
 M1 n1 = n1

ho2db_det1 < apply add_det1 to _ _ _ _ H23 H24.

Subgoal 3.2.2.1:

Variables: L M1 P HX dx lf_1 P3 HX1 O lf_2 Q Q1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
H22 : <O:nat>
H23 : <Q n1:add (HX n1) (dx n1) O>
H24 : <Q1 n1:add (HX1 n1) (dx n1) O>
============================
 <dx n1:nat>

Subgoal 3.2.2 is:
 M1 n1 = n1

ho2db_det1 < backchain nat_ignores_ctx.

Subgoal 3.2.2:

Variables: L M1 P dx lf_1 P3 HX1 O lf_2 Q Q1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh ->
          ho2db (M1 n1) hh (dvar dx)>
       (L n1)
H7 : <HX1 n1:nat>
H8 : fresh (M1 n1) O
H9 : le (s (HX1 n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX1 n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
H22 : <O:nat>
H23 : <Q n1:add (HX1 n1) (dx n1) O>
H24 : <Q1 n1:add (HX1 n1) (dx n1) O>
============================
 M1 n1 = n1

ho2db_det1 < apply ctx_unique2 to _ H5 H14.

Subgoal 3.2.2:

Variables: L dx lf_1 P3 HX1 O lf_2 Q Q1
IH : forall L M1 M2 D H P1 P2, ctx L H -> <L |- P1:ho2db M1 H D>* ->
       <L |- P2:ho2db M2 H D> -> M1 = M2
H1 : ctx (L n1) O
H5 : member
       <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
       (L n1)
H7 : <HX1 n1:nat>
H8 : fresh n1 O
H9 : le (s (HX1 n1)) O
H10 : <L n1 |- O:nat>*
H11 : <L n1 |- dx n1:nat>*
H12 : <L n1 |- lf_1 n1:add (HX1 n1) (dx n1) O>*
H14 : member
        <P3 n1:{hh:nat} {dx:nat} add (HX1 n1) dx hh -> ho2db n1 hh (dvar dx)>
        (L n1)
H16 : <HX1 n1:nat>
H18 : le (s (HX1 n1)) O
H19 : <L n1 |- O:nat>
H20 : <L n1 |- dx n1:nat>
H21 : <L n1 |- lf_2 n1:add (HX1 n1) (dx n1) O>
H22 : <O:nat>
H23 : <Q n1:add (HX1 n1) (dx n1) O>
H24 : <Q1 n1:add (HX1 n1) (dx n1) O>
============================
 n1 = n1

ho2db_det1 < search.
Proof completed.

Abella < Theorem ho2db_det1_simple : 
forall M1 M2 D P1 P2, <P1:ho2db M1 z D> -> <P2:ho2db M2 z D> -> M1 = M2.

============================
 forall M1 M2 D P1 P2, <P1:ho2db M1 z D> -> <P2:ho2db M2 z D> -> M1 = M2

ho2db_det1_simple < intros.

Variables: M1 M2 D P1 P2
H1 : <P1:ho2db M1 z D>
H2 : <P2:ho2db M2 z D>
============================
 M1 = M2

ho2db_det1_simple < apply ho2db_det1 to _ H1 H2.

Variables: M2 D P1 P2
H1 : <P1:ho2db M2 z D>
H2 : <P2:ho2db M2 z D>
============================
 M2 = M2

ho2db_det1_simple < search.
Proof completed.

Abella < Goodbye.