Welcome to Abella 2.0.3-dev
```Abella < Specification "str1".
```
```Abella < Define ctx : olist ->
prop by
ctx nil;
ctx ((p => q) :: L) := ctx L.
```
```Abella < Theorem ctx_mem :
forall L E, ctx L -> member E L -> E = p => q.
```
```
============================
forall L E, ctx L -> member E L -> E = p => q

ctx_mem < induction on 2.
```
```
IH : forall L E, ctx L -> member E L * -> E = p => q
============================
forall L E, ctx L -> member E L @ -> E = p => q

ctx_mem < intros.
```
```
Variables: L E
IH : forall L E, ctx L -> member E L * -> E = p => q
H1 : ctx L
H2 : member E L @
============================
E = p => q

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

Variables: E L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H1 : ctx (E :: L1)
============================
E = p => q

Subgoal 2 is:
E = p => q

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

Variables: L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H3 : ctx L1
============================
p => q = p => q

Subgoal 2 is:
E = p => q

ctx_mem < search.
```
```Subgoal 2:

Variables: E L1 B
IH : forall L E, ctx L -> member E L * -> E = p => q
H1 : ctx (B :: L1)
H3 : member E L1 *
============================
E = p => q

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

Variables: E L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H3 : member E L1 *
H4 : ctx L1
============================
E = p => q

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

Variables: L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H3 : member (p => q) L1 *
H4 : ctx L1
============================
p => q = p => q

ctx_mem < search.
Proof completed.
```
```Abella < Theorem indep :
(forall L, ctx L -> {L, p |- p} -> {L |- p}) /\
(forall L, ctx L -> {L, p |- q} -> {L |- q}) /\
(forall L, ctx L -> {L, p |- r} -> {L |- r}).
```
```
============================
(forall L, ctx L -> {L, p |- p} -> {L |- p}) /\
(forall L, ctx L -> {L, p |- q} -> {L |- q}) /\
(forall L, ctx L -> {L, p |- r} -> {L |- r})

indep < induction on 2 2 2.
```
```
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
(forall L, ctx L -> {L, p |- p}@ -> {L |- p}) /\
(forall L, ctx L -> {L, p |- q}@ -> {L |- q}) /\
(forall L, ctx L -> {L, p |- r}@ -> {L |- r})

indep < intros.
```
```
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
(forall L, ctx L -> {L, p |- p}@ -> {L |- p}) /\
(forall L, ctx L -> {L, p |- q}@ -> {L |- q}) /\
(forall L, ctx L -> {L, p |- r}@ -> {L |- r})

indep < split.
```
```Subgoal 1:

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
forall L, ctx L -> {L, p |- p}@ -> {L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < intros.
```
```Subgoal 1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H2 : {L, p |- p}@
============================
{L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

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

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- p}*
H4 : member F (p :: L)
============================
{L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H4.
```
```Subgoal 1.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p] |- p}*
============================
{L |- p}

Subgoal 1.2 is:
{L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

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

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
============================
{L |- p}

Subgoal 1.2 is:
{L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < skip.
```
```Subgoal 1.2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- p}*
H5 : member F L
============================
{L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < apply ctx_mem to _ H5.
```
```Subgoal 1.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p => q] |- p}*
H5 : member (p => q) L
============================
{L |- p}

Subgoal 2 is:
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.
```
```Subgoal 2:

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < intros.
```
```Subgoal 2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H2 : {L, p |- q}@
============================
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

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

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- q}*
H4 : member F (p :: L)
============================
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H4.
```
```Subgoal 2.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p] |- q}*
============================
{L |- q}

Subgoal 2.2 is:
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.
```
```Subgoal 2.2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- q}*
H5 : member F L
============================
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < apply ctx_mem to _ H5.
```
```Subgoal 2.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p => q] |- q}*
H5 : member (p => q) L
============================
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.
```
```Subgoal 2.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H5 : member (p => q) L
H6 : {L, p |- p}*
============================
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < apply IH to _ H6.
```
```Subgoal 2.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H5 : member (p => q) L
H6 : {L, p |- p}*
H7 : {L |- p}
============================
{L |- q}

Subgoal 3 is:
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < search.
```
```Subgoal 3:

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < intros.
```
```Subgoal 3:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H2 : {L, p |- r}@
============================
{L |- r}

indep < case H2.
```
```Subgoal 3.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, p => q |- r}*
============================
{L |- r}

Subgoal 3.2 is:
{L |- r}

Subgoal 3.3 is:
{L |- r}

indep < apply IH2 to _ H3.
```
```Subgoal 3.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, p => q |- r}*
H4 : {L, p => q |- r}
============================
{L |- r}

Subgoal 3.2 is:
{L |- r}

Subgoal 3.3 is:
{L |- r}

indep < search.
```
```Subgoal 3.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p |- q}*
============================
{L |- r}

Subgoal 3.3 is:
{L |- r}

indep < apply IH1 to _ H3.
```
```Subgoal 3.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p |- q}*
H4 : {L |- q}
============================
{L |- r}

Subgoal 3.3 is:
{L |- r}

indep < search.
```
```Subgoal 3.3:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- r}*
H4 : member F (p :: L)
============================
{L |- r}

indep < case H4.
```
```Subgoal 3.3.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p] |- r}*
============================
{L |- r}

Subgoal 3.3.2 is:
{L |- r}

indep < case H3.
```
```Subgoal 3.3.2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- r}*
H5 : member F L
============================
{L |- r}

indep < apply ctx_mem to _ H5.
```
```Subgoal 3.3.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p => q] |- r}*
H5 : member (p => q) L
============================
{L |- r}

indep < case H3.
Proof completed.
```
```Abella < Goodbye.
```