Welcome to Abella 2.0.5-dev.
```Abella < Define remove : olist -> o -> olist -> prop by
remove (A :: G) A G;
remove (B :: G) A (B :: D) := remove G A D.

```
```Abella < Theorem remove_incl :
forall G D A B, remove G A D -> member B D -> member B G.

```
```
============================
forall G D A B, remove G A D -> member B D -> member B G

remove_incl < induction on 1.
```
```
IH : forall G D A B, remove G A D * -> member B D -> member B G
============================
forall G D A B, remove G A D @ -> member B D -> member B G

remove_incl < intros.
```
```
Variables: G D A B
IH : forall G D A B, remove G A D * -> member B D -> member B G
H1 : remove G A D @
H2 : member B D
============================
member B G

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

Variables: D A B
IH : forall G D A B, remove G A D * -> member B D -> member B G
H2 : member B D
============================
member B (A :: D)

Subgoal 2 is:
member B (B1 :: G1)

remove_incl < search.
```
```Subgoal 2:

Variables: A B D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H2 : member B (B1 :: D1)
H3 : remove G1 A D1 *
============================
member B (B1 :: G1)

remove_incl < case H2.
```
```Subgoal 2.1:

Variables: A D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H3 : remove G1 A D1 *
============================
member B1 (B1 :: G1)

Subgoal 2.2 is:
member B (B1 :: G1)

remove_incl < search.
```
```Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H3 : remove G1 A D1 *
H4 : member B D1
============================
member B (B1 :: G1)

remove_incl < apply IH to H3 H4.
```
```Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H3 : remove G1 A D1 *
H4 : member B D1
H5 : member B G1
============================
member B (B1 :: G1)

remove_incl < search.
Proof completed.
```
```Abella < Theorem remove_charac :
forall G A D B, remove G A D -> member B G -> A = B \/ member B D.

```
```
============================
forall G A D B, remove G A D -> member B G -> A = B \/ member B D

remove_charac < induction on 1.
```
```
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
============================
forall G A D B, remove G A D @ -> member B G -> A = B \/ member B D

remove_charac < intros.
```
```
Variables: G A D B
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove G A D @
H2 : member B G
============================
A = B \/ member B D

remove_charac < case H1 (keep).
```
```Subgoal 1:

Variables: A D B
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (A :: D) A D @
H2 : member B (A :: D)
============================
A = B \/ member B D

Subgoal 2 is:
A = B \/ member B (B1 :: D1)

remove_charac < case H2.
```
```Subgoal 1.1:

Variables: A D
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (A :: D) A D @
============================
A = A \/ member A D

Subgoal 1.2 is:
A = B \/ member B D

Subgoal 2 is:
A = B \/ member B (B1 :: D1)

remove_charac < search.
```
```Subgoal 1.2:

Variables: A D B
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (A :: D) A D @
H3 : member B D
============================
A = B \/ member B D

Subgoal 2 is:
A = B \/ member B (B1 :: D1)

remove_charac < search.
```
```Subgoal 2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H2 : member B (B1 :: G1)
H3 : remove G1 A D1 *
============================
A = B \/ member B (B1 :: D1)

remove_charac < case H2.
```
```Subgoal 2.1:

Variables: A D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
============================
A = B1 \/ member B1 (B1 :: D1)

Subgoal 2.2 is:
A = B \/ member B (B1 :: D1)

remove_charac < search.
```
```Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
H4 : member B G1
============================
A = B \/ member B (B1 :: D1)

remove_charac < apply IH to H3 H4.
```
```Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
H4 : member B G1
H5 : A = B \/ member B D1
============================
A = B \/ member B (B1 :: D1)

remove_charac < case H5.
```
```Subgoal 2.2.1:

Variables: B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) B (B1 :: D1) @
H3 : remove G1 B D1 *
H4 : member B G1
============================
B = B \/ member B (B1 :: D1)

Subgoal 2.2.2 is:
A = B \/ member B (B1 :: D1)

remove_charac < search.
```
```Subgoal 2.2.2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
H4 : member B G1
H6 : member B D1
============================
A = B \/ member B (B1 :: D1)

remove_charac < search.
Proof completed.
```
```Abella < Kind fm, tm type.

```
```Abella < Type atm tm -> fm.

```
```Abella < Type and fm -> fm -> fm.

```
```Abella < Type top fm.

```
```Abella < Type imp fm -> fm -> fm.

```
```Abella < Type all (tm -> fm) -> fm.

```
```Abella < Type \$fm fm -> o.

```
```Abella < Define is_fm : fm -> prop by
is_fm (atm A);
is_fm (and A B) := is_fm A /\ is_fm B;
is_fm top;
is_fm (imp A B) := is_fm A /\ is_fm B;
is_fm (all A) := forall x, is_fm (A x).

```
```Abella < Type prog fm -> prop.

```
```Abella < Theorem prog_has_no_nablas :
forall F, nabla n, prog (F n) -> (exists E, F = x\E).

```
```
============================
forall F, nabla n, prog (F n) -> (exists E, F = x\E)

prog_has_no_nablas < skip.
Proof completed.
```
```Abella < Define seq : olist -> fm -> prop,
bch : olist -> fm -> tm -> prop by
seq L (atm A) := exists F, member (\$fm F) L /\ bch L F A;
seq L (atm A) := exists F, prog F /\ bch L F A;
seq L (and G1 G2) := seq L G1 /\ seq L G2;
seq L top;
seq L (imp F G) := seq (\$fm F :: L) G;
seq L (all A) := nabla x, seq L (A x);
bch L (atm A) A;
bch L (and F1 F2) A := bch L F1 A \/ bch L F2 A;
bch L (imp G F) A := seq L G /\ bch L F A;
bch L (all F) A := exists t, bch L (F t) A.

```
```Abella < Theorem \$monotone :
(forall L L' C, (forall E, member E L -> member E L') -> seq L C -> seq L' C) /\
(forall L L' F A, (forall E, member E L -> member E L') -> bch L F A ->
bch L' F A).

```
```
============================
(forall L L' C, (forall E, member E L -> member E L') -> seq L C ->
seq L' C) /\
(forall L L' F A, (forall E, member E L -> member E L') -> bch L F A ->
bch L' F A)

\$monotone < induction on 2 2.
```
```
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
============================
(forall L L' C, (forall E, member E L -> member E L') -> seq L C @ ->
seq L' C) /\
(forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A)

\$monotone < split.
```
```Subgoal 1:

IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
============================
forall L L' C, (forall E, member E L -> member E L') -> seq L C @ ->
seq L' C

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < intros.
```
```Subgoal 1:

Variables: L L' C
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L C @
============================
seq L' C

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < case H2 (keep).
```
```Subgoal 1.1:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : member (\$fm F) L
H4 : bch L F A *
============================
seq L' (atm A)

Subgoal 1.2 is:
seq L' (atm A)

Subgoal 1.3 is:
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply IH1 to H1 H4.
```
```Subgoal 1.1:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : member (\$fm F) L
H4 : bch L F A *
H5 : bch L' F A
============================
seq L' (atm A)

Subgoal 1.2 is:
seq L' (atm A)

Subgoal 1.3 is:
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply H1 to H3.
```
```Subgoal 1.1:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : member (\$fm F) L
H4 : bch L F A *
H5 : bch L' F A
H6 : member (\$fm F) L'
============================
seq L' (atm A)

Subgoal 1.2 is:
seq L' (atm A)

Subgoal 1.3 is:
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.2:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : prog F
H4 : bch L F A *
============================
seq L' (atm A)

Subgoal 1.3 is:
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply IH1 to H1 H4.
```
```Subgoal 1.2:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : prog F
H4 : bch L F A *
H5 : bch L' F A
============================
seq L' (atm A)

Subgoal 1.3 is:
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.3:

Variables: L L' G2 G1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (and G1 G2) @
H3 : seq L G1 *
H4 : seq L G2 *
============================
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply IH to H1 H3.
```
```Subgoal 1.3:

Variables: L L' G2 G1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (and G1 G2) @
H3 : seq L G1 *
H4 : seq L G2 *
H5 : seq L' G1
============================
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply IH to H1 H4.
```
```Subgoal 1.3:

Variables: L L' G2 G1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (and G1 G2) @
H3 : seq L G1 *
H4 : seq L G2 *
H5 : seq L' G1
H6 : seq L' G2
============================
seq L' (and G1 G2)

Subgoal 1.4 is:
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.4:

Variables: L L'
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L top @
============================
seq L' top

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.5:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
============================
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < assert forall E, member E (\$fm F :: L) -> member E (\$fm F :: L').
```
```Subgoal 1.5.1:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
============================
forall E, member E (\$fm F :: L) -> member E (\$fm F :: L')

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < intros.
```
```Subgoal 1.5.1:

Variables: L L' G F E
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
H4 : member E (\$fm F :: L)
============================
member E (\$fm F :: L')

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < case H4.
```
```Subgoal 1.5.1.1:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
============================
member (\$fm F) (\$fm F :: L')

Subgoal 1.5.1.2 is:
member E (\$fm F :: L')

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.5.1.2:

Variables: L L' G F E
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
H5 : member E L
============================
member E (\$fm F :: L')

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply H1 to H5.
```
```Subgoal 1.5.1.2:

Variables: L L' G F E
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
H5 : member E L
H6 : member E L'
============================
member E (\$fm F :: L')

Subgoal 1.5 is:
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.5:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
H4 : forall E, member E (\$fm F :: L) -> member E (\$fm F :: L')
============================
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply IH to H4 H3.
```
```Subgoal 1.5:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq (\$fm F :: L) G *
H4 : forall E, member E (\$fm F :: L) -> member E (\$fm F :: L')
H5 : seq (\$fm F :: L') G
============================
seq L' (imp F G)

Subgoal 1.6 is:
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 1.6:

Variables: L L' A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (all A) @
H3 : seq L (A n1) *
============================
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < apply IH to H1 H3.
```
```Subgoal 1.6:

Variables: L L' A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (all A) @
H3 : seq L (A n1) *
H4 : seq L' (A n1)
============================
seq L' (all A)

Subgoal 2 is:
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < search.
```
```Subgoal 2:

IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
============================
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
bch L' F A

\$monotone < intros.
```
```Subgoal 2:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L F A @
============================
bch L' F A

\$monotone < case H2 (keep).
```
```Subgoal 2.1:

Variables: L L' A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (atm A) A @
============================
bch L' (atm A) A

Subgoal 2.2 is:
bch L' (and F1 F2) A

Subgoal 2.3 is:
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < search.
```
```Subgoal 2.2:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H3 : bch L F1 A * \/ bch L F2 A *
============================
bch L' (and F1 F2) A

Subgoal 2.3 is:
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < case H3.
```
```Subgoal 2.2.1:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F1 A *
============================
bch L' (and F1 F2) A

Subgoal 2.2.2 is:
bch L' (and F1 F2) A

Subgoal 2.3 is:
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < apply IH1 to H1 H4.
```
```Subgoal 2.2.1:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F1 A *
H5 : bch L' F1 A
============================
bch L' (and F1 F2) A

Subgoal 2.2.2 is:
bch L' (and F1 F2) A

Subgoal 2.3 is:
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < search.
```
```Subgoal 2.2.2:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F2 A *
============================
bch L' (and F1 F2) A

Subgoal 2.3 is:
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < apply IH1 to H1 H4.
```
```Subgoal 2.2.2:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F2 A *
H5 : bch L' F2 A
============================
bch L' (and F1 F2) A

Subgoal 2.3 is:
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < search.
```
```Subgoal 2.3:

Variables: L L' A F1 G
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (imp G F1) A @
H3 : seq L G *
H4 : bch L F1 A *
============================
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < apply IH to H1 H3.
```
```Subgoal 2.3:

Variables: L L' A F1 G
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (imp G F1) A @
H3 : seq L G *
H4 : bch L F1 A *
H5 : seq L' G
============================
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < apply IH1 to H1 H4.
```
```Subgoal 2.3:

Variables: L L' A F1 G
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (imp G F1) A @
H3 : seq L G *
H4 : bch L F1 A *
H5 : seq L' G
H6 : bch L' F1 A
============================
bch L' (imp G F1) A

Subgoal 2.4 is:
bch L' (all F1) A

\$monotone < search.
```
```Subgoal 2.4:

Variables: L L' A t F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (all F1) A @
H3 : bch L (F1 t) A *
============================
bch L' (all F1) A

\$monotone < apply IH1 to H1 H3.
```
```Subgoal 2.4:

Variables: L L' A t F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (all F1) A @
H3 : bch L (F1 t) A *
H4 : bch L' (F1 t) A
============================
bch L' (all F1) A

\$monotone < search.
Proof completed.
```
```Abella < Split \$monotone as monotone_seq, monotone_bch.
Theorem monotone_seq :
forall L L' C, (forall E, member E L -> member E L') -> seq L C -> seq L' C.
Theorem monotone_bch :
forall L L' F A, (forall E, member E L -> member E L') -> bch L F A ->
bch L' F A.

```
```Abella < Theorem \$weakening :
(forall L L' B G, remove L' B L -> seq L G -> seq L' G) /\
(forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A).

```
```
============================
(forall L L' B G, remove L' B L -> seq L G -> seq L' G) /\
(forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A)

\$weakening < split.
```
```Subgoal 1:

============================
forall L L' B G, remove L' B L -> seq L G -> seq L' G

Subgoal 2 is:
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

\$weakening < intros.
```
```Subgoal 1:

Variables: L L' B G
H1 : remove L' B L
H2 : seq L G
============================
seq L' G

Subgoal 2 is:
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

\$weakening < assert forall E, member E L -> member E L'.
```
```Subgoal 1.1:

Variables: L L' B G
H1 : remove L' B L
H2 : seq L G
============================
forall E, member E L -> member E L'

Subgoal 1 is:
seq L' G

Subgoal 2 is:
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

\$weakening < intros.
```
```Subgoal 1.1:

Variables: L L' B G E
H1 : remove L' B L
H2 : seq L G
H3 : member E L
============================
member E L'

Subgoal 1 is:
seq L' G

Subgoal 2 is:
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

\$weakening < backchain remove_incl.
```
```Subgoal 1:

Variables: L L' B G
H1 : remove L' B L
H2 : seq L G
H3 : forall E, member E L -> member E L'
============================
seq L' G

Subgoal 2 is:
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

\$weakening < backchain monotone_seq.
```
```Subgoal 2:

============================
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

\$weakening < intros.
```
```Subgoal 2:

Variables: L L' B F A
H1 : remove L' B L
H2 : bch L F A
============================
bch L' F A

\$weakening < assert forall E, member E L -> member E L'.
```
```Subgoal 2.1:

Variables: L L' B F A
H1 : remove L' B L
H2 : bch L F A
============================
forall E, member E L -> member E L'

Subgoal 2 is:
bch L' F A

\$weakening < intros.
```
```Subgoal 2.1:

Variables: L L' B F A E
H1 : remove L' B L
H2 : bch L F A
H3 : member E L
============================
member E L'

Subgoal 2 is:
bch L' F A

\$weakening < backchain remove_incl.
```
```Subgoal 2:

Variables: L L' B F A
H1 : remove L' B L
H2 : bch L F A
H3 : forall E, member E L -> member E L'
============================
bch L' F A

\$weakening < backchain monotone_bch.
Proof completed.
```
```Abella < Split \$weakening as weakening_seq, weakening_bch.
Theorem weakening_seq : forall L L' B G, remove L' B L -> seq L G -> seq L' G.
Theorem weakening_bch :
forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A.

```
```Abella < Theorem member_inst :
forall F L, nabla n, member (F n) (L n) -> (forall t, member (F t) (L t)).

```
```
============================
forall F L, nabla n, member (F n) (L n) -> (forall t, member (F t) (L t))

member_inst < induction on 1.
```
```
IH : forall F L, nabla n, member (F n) (L n) * ->
(forall t, member (F t) (L t))
============================
forall F L, nabla n, member (F n) (L n) @ -> (forall t, member (F t) (L t))

member_inst < intros.
```
```
Variables: F L t
IH : forall F L, nabla n, member (F n) (L n) * ->
(forall t, member (F t) (L t))
H1 : member (F n1) (L n1) @
============================
member (F t) (L t)

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

Variables: F t L1
IH : forall F L, nabla n, member (F n) (L n) * ->
(forall t, member (F t) (L t))
============================
member (F t) (F t :: L1 t)

Subgoal 2 is:
member (F t) (B t :: L1 t)

member_inst < search.
```
```Subgoal 2:

Variables: F t L1 B
IH : forall F L, nabla n, member (F n) (L n) * ->
(forall t, member (F t) (L t))
H2 : member (F n1) (L1 n1) *
============================
member (F t) (B t :: L1 t)

member_inst < apply IH to H2.
```
```Subgoal 2:

Variables: F t L1 B
IH : forall F L, nabla n, member (F n) (L n) * ->
(forall t, member (F t) (L t))
H2 : member (F n1) (L1 n1) *
H3 : forall t, member (F t) (L1 t)
============================
member (F t) (B t :: L1 t)

member_inst < apply H3 with t = t.
```
```Subgoal 2:

Variables: F t L1 B
IH : forall F L, nabla n, member (F n) (L n) * ->
(forall t, member (F t) (L t))
H2 : member (F n1) (L1 n1) *
H3 : forall t, member (F t) (L1 t)
H4 : member (F t) (L1 t)
============================
member (F t) (B t :: L1 t)

member_inst < search.
Proof completed.
```
```Abella < Theorem \$inst :
(forall L G, nabla n, seq (L n) (G n) -> (forall t, seq (L t) (G t))) /\
(forall L F A, nabla n, bch (L n) (F n) (A n) ->
(forall t, bch (L t) (F t) (A t))).

```
```
============================
(forall L G, nabla n, seq (L n) (G n) -> (forall t, seq (L t) (G t))) /\
(forall L F A, nabla n, bch (L n) (F n) (A n) ->
(forall t, bch (L t) (F t) (A t)))

\$inst < induction on 1 1.
```
```
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
============================
(forall L G, nabla n, seq (L n) (G n) @ -> (forall t, seq (L t) (G t))) /\
(forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t)))

\$inst < split.
```
```Subgoal 1:

IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
============================
forall L G, nabla n, seq (L n) (G n) @ -> (forall t, seq (L t) (G t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < intros.
```
```Subgoal 1:

Variables: L G t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H1 : seq (L n1) (G n1) @
============================
seq (L t) (G t)

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < case H1.
```
```Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : member (\$fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
============================
seq (L t) (atm (A t))

Subgoal 1.2 is:
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply IH1 to H3.
```
```Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : member (\$fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
============================
seq (L t) (atm (A t))

Subgoal 1.2 is:
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply member_inst to H2.
```
```Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : member (\$fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
H5 : forall t, member (\$fm (F t)) (L t)
============================
seq (L t) (atm (A t))

Subgoal 1.2 is:
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H4 with t = t.
```
```Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : member (\$fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
H5 : forall t, member (\$fm (F t)) (L t)
H6 : bch (L t) (F t) (A t)
============================
seq (L t) (atm (A t))

Subgoal 1.2 is:
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H5 with t = t.
```
```Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : member (\$fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
H5 : forall t, member (\$fm (F t)) (L t)
H6 : bch (L t) (F t) (A t)
H7 : member (\$fm (F t)) (L t)
============================
seq (L t) (atm (A t))

Subgoal 1.2 is:
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < search.
```
```Subgoal 1.2:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : prog (F n1)
H3 : bch (L n1) (F n1) (A n1) *
============================
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply IH1 to H3.
```
```Subgoal 1.2:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : prog (F n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
============================
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply prog_has_no_nablas to H2.
```
```Subgoal 1.2:

Variables: L t A E
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : prog E
H3 : bch (L n1) E (A n1) *
H4 : forall t, bch (L t) E (A t)
============================
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H4 with t = t.
```
```Subgoal 1.2:

Variables: L t A E
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : prog E
H3 : bch (L n1) E (A n1) *
H4 : forall t, bch (L t) E (A t)
H5 : bch (L t) E (A t)
============================
seq (L t) (atm (A t))

Subgoal 1.3 is:
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < search.
```
```Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
============================
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply IH to H2.
```
```Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
============================
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply IH to H3.
```
```Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
H5 : forall t, seq (L t) (G2 t)
============================
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H4 with t = t.
```
```Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
H5 : forall t, seq (L t) (G2 t)
H6 : seq (L t) (G1 t)
============================
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H5 with t = t.
```
```Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
H5 : forall t, seq (L t) (G2 t)
H6 : seq (L t) (G1 t)
H7 : seq (L t) (G2 t)
============================
seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < search.
```
```Subgoal 1.4:

Variables: L t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
============================
seq (L t) top

Subgoal 1.5 is:
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < search.
```
```Subgoal 1.5:

Variables: L t G1 F
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (\$fm (F n1) :: L n1) (G1 n1) *
============================
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply IH to H2.
```
```Subgoal 1.5:

Variables: L t G1 F
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (\$fm (F n1) :: L n1) (G1 n1) *
H3 : forall t, seq (\$fm (F t) :: L t) (G1 t)
============================
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H3 with t = t.
```
```Subgoal 1.5:

Variables: L t G1 F
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (\$fm (F n1) :: L n1) (G1 n1) *
H3 : forall t, seq (\$fm (F t) :: L t) (G1 t)
H4 : seq (\$fm (F t) :: L t) (G1 t)
============================
seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < search.
```
```Subgoal 1.6:

Variables: L t A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (A n1 n2) *
============================
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply IH to H2.
```
```Subgoal 1.6:

Variables: L t A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (A n1 n2) *
H3 : forall t, seq (L t) (A t n2)
============================
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < apply H3 with t = t.
```
```Subgoal 1.6:

Variables: L t A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (A n1 n2) *
H3 : forall t, seq (L t) (A t n2)
H4 : seq (L t) (A t n2)
============================
seq (L t) (all (A t))

Subgoal 2 is:
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < search.
```
```Subgoal 2:

IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
============================
forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
(forall t, bch (L t) (F t) (A t))

\$inst < intros.
```
```Subgoal 2:

Variables: L F A t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H1 : bch (L n1) (F n1) (A n1) @
============================
bch (L t) (F t) (A t)

\$inst < case H1.
```
```Subgoal 2.1:

Variables: L A t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
============================
bch (L t) (atm (A t)) (A t)

Subgoal 2.2 is:
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < search.
```
```Subgoal 2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1) (A n1) * \/ bch (L n1) (F2 n1) (A n1) *
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < case H2.
```
```Subgoal 2.2.1:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F1 n1) (A n1) *
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.2.2 is:
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply IH1 to H3.
```
```Subgoal 2.2.1:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, bch (L t) (F1 t) (A t)
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.2.2 is:
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply H4 with t = t.
```
```Subgoal 2.2.1:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, bch (L t) (F1 t) (A t)
H5 : bch (L t) (F1 t) (A t)
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.2.2 is:
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < search.
```
```Subgoal 2.2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F2 n1) (A n1) *
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply IH1 to H3.
```
```Subgoal 2.2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F2 n1) (A n1) *
H4 : forall t, bch (L t) (F2 t) (A t)
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply H4 with t = t.
```
```Subgoal 2.2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F2 n1) (A n1) *
H4 : forall t, bch (L t) (F2 t) (A t)
H5 : bch (L t) (F2 t) (A t)
============================
bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < search.
```
```Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
============================
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply IH to H2.
```
```Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
============================
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply IH1 to H3.
```
```Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
H5 : forall t, bch (L t) (F1 t) (A t)
============================
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply H4 with t = t.
```
```Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
H5 : forall t, bch (L t) (F1 t) (A t)
H6 : seq (L t) (G t)
============================
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < apply H5 with t = t.
```
```Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
H5 : forall t, bch (L t) (F1 t) (A t)
H6 : seq (L t) (G t)
H7 : bch (L t) (F1 t) (A t)
============================
bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
bch (L t) (all (F1 t)) (A t)

\$inst < search.
```
```Subgoal 2.4:

Variables: L A t t1 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1 (t1 n1)) (A n1) *
============================
bch (L t) (all (F1 t)) (A t)

\$inst < apply IH1 to H2.
```
```Subgoal 2.4:

Variables: L A t t1 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1 (t1 n1)) (A n1) *
H3 : forall t, bch (L t) (F1 t (t1 t)) (A t)
============================
bch (L t) (all (F1 t)) (A t)

\$inst < apply H3 with t = t.
```
```Subgoal 2.4:

Variables: L A t t1 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
(forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1 (t1 n1)) (A n1) *
H3 : forall t, bch (L t) (F1 t (t1 t)) (A t)
H4 : bch (L t) (F1 t (t1 t)) (A t)
============================
bch (L t) (all (F1 t)) (A t)

\$inst < search.
Proof completed.
```
```Abella < Split \$inst as inst_seq, inst_bch.
Theorem inst_seq :
forall L G, nabla n, seq (L n) (G n) -> (forall t, seq (L t) (G t)).
Theorem inst_bch :
forall L F A, nabla n, bch (L n) (F n) (A n) ->
(forall t, bch (L t) (F t) (A t)).

```
```Abella < Theorem \$cut :
(forall L K F G, is_fm F -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G) /\
(forall L K F F' A, is_fm F -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A) /\
(forall L F A, is_fm F -> seq L F -> bch L F A -> seq L (atm A)).

```
```
============================
(forall L K F G, is_fm F -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G) /\
(forall L K F F' A, is_fm F -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A) /\
(forall L F A, is_fm F -> seq L F -> bch L F A -> seq L (atm A))

\$cut < induction on 1 1 1.
```
```
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
============================
(forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G) /\
(forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A) /\
(forall L F A, is_fm F @ -> seq L F -> bch L F A -> seq L (atm A))

\$cut < induction on 4 4 3.
```
```
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
(forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K -> seq L G @@ ->
seq K G) /\
(forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A) /\
(forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A))

\$cut < split.
```
```Subgoal 1:

IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K -> seq L G @@ ->
seq K G

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < intros.
```
```Subgoal 1:

Variables: L K F G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L G @@
============================
seq K G

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H4 (keep).
```
```Subgoal 1.1:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (atm A) @@
H5 : member (\$fm F1) L
H6 : bch L F1 A **
============================
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply remove_charac to H3 H5.
```
```Subgoal 1.1:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (atm A) @@
H5 : member (\$fm F1) L
H6 : bch L F1 A **
H7 : \$fm F = \$fm F1 \/ member (\$fm F1) K
============================
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H7.
```
```Subgoal 1.1.1:

Variables: L K F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F1 @
H2 : seq K F1
H3 : remove L (\$fm F1) K
H4 : seq L (atm A) @@
H5 : member (\$fm F1) L
H6 : bch L F1 A **
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H1 (keep).
```
```Subgoal 1.1.1.1:

Variables: L K A A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (atm A1) @
H2 : seq K (atm A1)
H3 : remove L (\$fm (atm A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (atm A1)) L
H6 : bch L (atm A1) A **
============================
seq K (atm A)

Subgoal 1.1.1.2 is:
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H6.
```
```Subgoal 1.1.1.1:

Variables: L K A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (atm A) @
H2 : seq K (atm A)
H3 : remove L (\$fm (atm A)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (atm A)) L
============================
seq K (atm A)

Subgoal 1.1.1.2 is:
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.1.1.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
============================
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H6 (keep).
```
```Subgoal 1.1.1.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H10 : bch L A1 A ** \/ bch L B A **
============================
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H10.
```
```Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
============================
seq K (atm A)

Subgoal 1.1.1.2.2 is:
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H11.
```
```Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
H12 : bch K A1 A
============================
seq K (atm A)

Subgoal 1.1.1.2.2 is:
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H2.
```
```Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
H12 : bch K A1 A
H13 : seq K A1
H14 : seq K B
============================
seq K (atm A)

Subgoal 1.1.1.2.2 is:
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH2 to H8 H13 H12.
```
```Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
H12 : bch K A1 A
H13 : seq K A1
H14 : seq K B
H15 : seq K (atm A)
============================
seq K (atm A)

Subgoal 1.1.1.2.2 is:
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
============================
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H11.
```
```Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
H12 : bch K B A
============================
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H2.
```
```Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
H12 : bch K B A
H13 : seq K A1
H14 : seq K B
============================
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH2 to H9 H14 H12.
```
```Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L (\$fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
H12 : bch K B A
H13 : seq K A1
H14 : seq K B
H15 : seq K (atm A)
============================
seq K (atm A)

Subgoal 1.1.1.3 is:
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.1.1.3:

Variables: L K A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm top @
H2 : seq K top
H3 : remove L (\$fm top) K
H4 : seq L (atm A) @@
H5 : member (\$fm top) L
H6 : bch L top A **
============================
seq K (atm A)

Subgoal 1.1.1.4 is:
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H6.
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H6 : bch L (imp A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H6.
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH3 to H1 H2 H3 H10.
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H11.
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H2 (keep).
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
H14 : seq (\$fm A1 :: K) B
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH to H8 H12 _ H14.
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
H14 : seq (\$fm A1 :: K) B
H15 : seq K B
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH2 to H9 H15 H13.
```
```Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L (\$fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
H14 : seq (\$fm A1 :: K) B
H15 : seq K B
H16 : seq K (atm A)
============================
seq K (atm A)

Subgoal 1.1.1.5 is:
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.1.1.5:

Variables: L K A A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H2 : seq K (all A1)
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H6 : bch L (all A1) A **
H8 : forall x, is_fm (A1 x) *
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H6.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H2 : seq K (all A1)
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H9.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H2 : seq K (all A1)
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H2.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply inst_seq to H11.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply H12 with t = t.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
H13 : seq K (A1 t)
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply H8 with x = t.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
H13 : seq K (A1 t)
H14 : is_fm (A1 t) *
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH2 to H14 H13 H10.
```
```Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L (\$fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member (\$fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
H13 : seq K (A1 t)
H14 : is_fm (A1 t) *
H15 : seq K (atm A)
============================
seq K (atm A)

Subgoal 1.1.2 is:
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (atm A) @@
H5 : member (\$fm F1) L
H6 : bch L F1 A **
H8 : member (\$fm F1) K
============================
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H6.
```
```Subgoal 1.1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (atm A) @@
H5 : member (\$fm F1) L
H6 : bch L F1 A **
H8 : member (\$fm F1) K
H9 : bch K F1 A
============================
seq K (atm A)

Subgoal 1.2 is:
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (atm A) @@
H5 : prog F1
H6 : bch L F1 A **
============================
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H6.
```
```Subgoal 1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (atm A) @@
H5 : prog F1
H6 : bch L F1 A **
H7 : bch K F1 A
============================
seq K (atm A)

Subgoal 1.3 is:
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.3:

Variables: L K F G2 G1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (and G1 G2) @@
H5 : seq L G1 **
H6 : seq L G2 **
============================
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH3 to H1 H2 H3 H5.
```
```Subgoal 1.3:

Variables: L K F G2 G1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (and G1 G2) @@
H5 : seq L G1 **
H6 : seq L G2 **
H7 : seq K G1
============================
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH3 to H1 H2 H3 H6.
```
```Subgoal 1.3:

Variables: L K F G2 G1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (and G1 G2) @@
H5 : seq L G1 **
H6 : seq L G2 **
H7 : seq K G1
H8 : seq K G2
============================
seq K (and G1 G2)

Subgoal 1.4 is:
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.4:

Variables: L K F
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L top @@
============================
seq K top

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq (\$fm F1 :: L) G1 **
============================
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < assert remove (\$fm F1 :: L) (\$fm F) (\$fm F1 :: K).
```
```Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq (\$fm F1 :: L) G1 **
H6 : remove (\$fm F1 :: L) (\$fm F) (\$fm F1 :: K)
============================
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < assert seq (\$fm F1 :: K) F.
```
```Subgoal 1.5.1:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq (\$fm F1 :: L) G1 **
H6 : remove (\$fm F1 :: L) (\$fm F) (\$fm F1 :: K)
============================
seq (\$fm F1 :: K) F

Subgoal 1.5 is:
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < backchain weakening_seq.
```
```Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq (\$fm F1 :: L) G1 **
H6 : remove (\$fm F1 :: L) (\$fm F) (\$fm F1 :: K)
H7 : seq (\$fm F1 :: K) F
============================
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH3 to H1 H7 H6 H5.
```
```Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq (\$fm F1 :: L) G1 **
H6 : remove (\$fm F1 :: L) (\$fm F) (\$fm F1 :: K)
H7 : seq (\$fm F1 :: K) F
H8 : seq (\$fm F1 :: K) G1
============================
seq K (imp F1 G1)

Subgoal 1.6 is:
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 1.6:

Variables: L K F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (all A) @@
H5 : seq L (A n1) **
============================
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH3 to H1 H2 H3 H5.
```
```Subgoal 1.6:

Variables: L K F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : seq L (all A) @@
H5 : seq L (A n1) **
H6 : seq K (A n1)
============================
seq K (all A)

Subgoal 2 is:
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 2:

IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A @@ -> bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < intros.
```
```Subgoal 2:

Variables: L K F F' A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L F' A @@
============================
bch K F' A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H4 (keep).
```
```Subgoal 2.1:

Variables: L K F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (atm A) A @@
============================
bch K (atm A) A

Subgoal 2.2 is:
bch K (and F1 F2) A

Subgoal 2.3 is:
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 2.2:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (and F1 F2) A @@
H5 : bch L F1 A ** \/ bch L F2 A **
============================
bch K (and F1 F2) A

Subgoal 2.3 is:
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < case H5.
```
```Subgoal 2.2.1:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F1 A **
============================
bch K (and F1 F2) A

Subgoal 2.2.2 is:
bch K (and F1 F2) A

Subgoal 2.3 is:
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H6.
```
```Subgoal 2.2.1:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F1 A **
H7 : bch K F1 A
============================
bch K (and F1 F2) A

Subgoal 2.2.2 is:
bch K (and F1 F2) A

Subgoal 2.3 is:
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 2.2.2:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F2 A **
============================
bch K (and F1 F2) A

Subgoal 2.3 is:
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H6.
```
```Subgoal 2.2.2:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F2 A **
H7 : bch K F2 A
============================
bch K (and F1 F2) A

Subgoal 2.3 is:
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 2.3:

Variables: L K F A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (imp G F1) A @@
H5 : seq L G **
H6 : bch L F1 A **
============================
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH3 to H1 H2 H3 H5.
```
```Subgoal 2.3:

Variables: L K F A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (imp G F1) A @@
H5 : seq L G **
H6 : bch L F1 A **
H7 : seq K G
============================
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H6.
```
```Subgoal 2.3:

Variables: L K F A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (imp G F1) A @@
H5 : seq L G **
H6 : bch L F1 A **
H7 : seq K G
H8 : bch K F1 A
============================
bch K (imp G F1) A

Subgoal 2.4 is:
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 2.4:

Variables: L K F A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (all F1) A @@
H5 : bch L (F1 t) A **
============================
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < apply IH4 to H1 H2 H3 H5.
```
```Subgoal 2.4:

Variables: L K F A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L (\$fm F) K
H4 : bch L (all F1) A @@
H5 : bch L (F1 t) A **
H6 : bch K (F1 t) A
============================
bch K (all F1) A

Subgoal 3 is:
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < search.
```
```Subgoal 3:

IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

\$cut < intros.
```
```Subgoal 3:

Variables: L F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq L F
H3 : bch L F A @@
============================
seq L (atm A)

\$cut < case H3 (keep).
```
```Subgoal 3.1:

Variables: L A
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (atm A) @
H2 : seq L (atm A)
H3 : bch L (atm A) A @@
============================
seq L (atm A)

Subgoal 3.2 is:
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < search.
```
```Subgoal 3.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H4 : bch L F1 A ** \/ bch L F2 A **
============================
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H4.
```
```Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
============================
seq L (atm A)

Subgoal 3.2.2 is:
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H1 (keep).
```
```Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
============================
seq L (atm A)

Subgoal 3.2.2 is:
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H2 (keep).
```
```Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
============================
seq L (atm A)

Subgoal 3.2.2 is:
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < apply IH2 to H6 H8 H5.
```
```Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
H10 : seq L (atm A)
============================
seq L (atm A)

Subgoal 3.2.2 is:
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < search.
```
```Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
============================
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H1 (keep).
```
```Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
============================
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H2 (keep).
```
```Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
============================
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < apply IH2 to H7 H9 H5.
```
```Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
H10 : seq L (atm A)
============================
seq L (atm A)

Subgoal 3.3 is:
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < search.
```
```Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
============================
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H1 (keep).
```
```Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
============================
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < case H2 (keep).
```
```Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
H8 : seq (\$fm G :: L) F1
============================
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < apply IH to H6 H4 _ H8.
```
```Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
H8 : seq (\$fm G :: L) F1
H9 : seq L F1
============================
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < apply IH2 to H7 H9 H5.
```
```Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
H8 : seq (\$fm G :: L) F1
H9 : seq L F1
H10 : seq L (atm A)
============================
seq L (atm A)

Subgoal 3.4 is:
seq L (atm A)

\$cut < search.
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
============================
seq L (atm A)

\$cut < case H1 (keep).
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
============================
seq L (atm A)

\$cut < case H2 (keep).
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
============================
seq L (atm A)

\$cut < apply H5 with x = t.
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
============================
seq L (atm A)

\$cut < apply inst_seq to H6.
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
H8 : forall t, seq L (F1 t)
============================
seq L (atm A)

\$cut < apply H8 with t = t.
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
H8 : forall t, seq L (F1 t)
H9 : seq L (F1 t)
============================
seq L (atm A)

\$cut < apply IH2 to H7 H9 H4.
```
```Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L (\$fm F) K ->
bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
H8 : forall t, seq L (F1 t)
H9 : seq L (F1 t)
H10 : seq L (atm A)
============================
seq L (atm A)

\$cut < search.
Proof completed.
```
```Abella < Split \$cut as cut, cut_commutative, cut_principal.
Theorem cut :
forall L K F G, is_fm F -> seq K F -> remove L (\$fm F) K -> seq L G ->
seq K G.
Theorem cut_commutative :
forall L K F F' A, is_fm F -> seq K F -> remove L (\$fm F) K ->
bch L F' A -> bch K F' A.
Theorem cut_principal :
forall L F A, is_fm F -> seq L F -> bch L F A -> seq L (atm A).

```
```Abella <
```