Welcome to Abella 2.0.5-dev

Abella < Define app : (list A) -> (list A) -> (list A) -> prop by 
app nil L L;
app (X :: L1) L2 (X :: L3) := app L1 L2 L3.

Abella < Theorem app_det [A] : 
forall L1 L2 L3 L3', app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'.

============================
 forall L1 L2 L3 L3', app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'

app_det < induction on 1.

IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
============================
 forall L1 L2 L3 L3', app L1 L2 L3 @ -> app L1 L2 L3' -> L3 = L3'

app_det < intros.

Variables: L1 L2 L3 L3'
IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
H1 : app L1 L2 L3 @
H2 : app L1 L2 L3'
============================
 L3 = L3'

app_det < case H1.

Subgoal 1:

Variables: L3 L3'
IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
H2 : app nil L3 L3'
============================
 L3 = L3'

Subgoal 2 is:
 X :: L6 = L3'

app_det < case H2.

Subgoal 1:

Variables: L3'
IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
============================
 L3' = L3'

Subgoal 2 is:
 X :: L6 = L3'

app_det < search.

Subgoal 2:

Variables: L2 L3' L6 X L4
IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
H2 : app (X :: L4) L2 L3'
H3 : app L4 L2 L6 *
============================
 X :: L6 = L3'

app_det < case H2.

Subgoal 2:

Variables: L2 L6 X L4 L8
IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
H3 : app L4 L2 L6 *
H4 : app L4 L2 L8
============================
 X :: L6 = X :: L8

app_det < apply IH to H3 H4.

Subgoal 2:

Variables: L2 X L4 L8
IH : forall L1 L2 L3 L3', app L1 L2 L3 * -> app L1 L2 L3' -> L3 = L3'
H3 : app L4 L2 L8 *
H4 : app L4 L2 L8
============================
 X :: L8 = X :: L8

app_det < search.
Proof completed.

Abella < Kind nat Type.

Abella < Theorem app_det_nat : 
forall L1 L2 L3 L3', app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'.

============================
 forall L1 L2 L3 L3', app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'

app_det_nat < intros.

Variables: L1 L2 L3 L3'
H1 : app L1 L2 L3
H2 : app L1 L2 L3'
============================
 L3 = L3'

app_det_nat < apply app_det to H1 H2.

Variables: L1 L2 L3'
H1 : app L1 L2 L3'
H2 : app L1 L2 L3'
============================
 L3' = L3'

app_det_nat < search.
Proof completed.

Abella < Theorem app_det_list [B] : 
forall L1 L2 L3 L3', app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'.

============================
 forall L1 L2 L3 L3', app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'

app_det_list < intros.

Variables: L1 L2 L3 L3'
H1 : app L1 L2 L3
H2 : app L1 L2 L3'
============================
 L3 = L3'

app_det_list < apply app_det to H1 H2.

Variables: L1 L2 L3'
H1 : app L1 L2 L3'
H2 : app L1 L2 L3'
============================
 L3' = L3'

app_det_list < search.
Proof completed.

Abella <