Welcome to Abella 2.0.4-dev
Abella < Specification "cut".
Reading specification "cut"

Abella < Define ctx : olist -> prop by 
ctx nil;
ctx (hyp A :: L) := ctx L.

Abella < Theorem ctx_lemma : 
forall E L, ctx L -> member E L -> (exists A, E = hyp A).


============================
 forall E L, ctx L -> member E L -> (exists A, E = hyp A)

ctx_lemma < induction on 1.

IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
============================
 forall E L, ctx L @ -> member E L -> (exists A, E = hyp A)

ctx_lemma < intros.

Variables: E L
IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
H1 : ctx L @
H2 : member E L
============================
 exists A, E = hyp A

ctx_lemma < case H1.
Subgoal 1:

Variables: E
IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
H2 : member E nil
============================
 exists A, E = hyp A

Subgoal 2 is:
 exists A, E = hyp A

ctx_lemma < case H2.
Subgoal 2:

Variables: E L1 A
IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
H2 : member E (hyp A :: L1)
H3 : ctx L1 *
============================
 exists A, E = hyp A

ctx_lemma < case H2.
Subgoal 2.1:

Variables: L1 A
IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
H3 : ctx L1 *
============================
 exists A1, hyp A = hyp A1

Subgoal 2.2 is:
 exists A, E = hyp A

ctx_lemma < search.
Subgoal 2.2:

Variables: E L1 A
IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
H3 : ctx L1 *
H4 : member E L1
============================
 exists A, E = hyp A

ctx_lemma < apply IH to H3 H4.
Subgoal 2.2:

Variables: L1 A A1
IH : forall E L, ctx L * -> member E L -> (exists A, E = hyp A)
H3 : ctx L1 *
H4 : member (hyp A1) L1
============================
 exists A, hyp A1 = hyp A

ctx_lemma < search.
Proof completed.
Abella < Theorem bot_inv : 
forall L C, ctx L -> {L |- conc bot} -> {L |- conc C}.


============================
 forall L C, ctx L -> {L |- conc bot} -> {L |- conc C}

bot_inv < induction on 2.

IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
============================
 forall L C, ctx L -> {L |- conc bot}@ -> {L |- conc C}

bot_inv < intros.

Variables: L C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H2 : {L |- conc bot}@
============================
 {L |- conc C}

bot_inv < case H2.
Subgoal 1:

Variables: L C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
 {L |- conc C}

Subgoal 2 is:
 {L |- conc C}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 2:

Variables: L C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
 {L |- conc C}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 3:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc bot}*
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < apply IH to _ H4 with C = C.
Subgoal 3:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc bot}*
H5 : {L, hyp A, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 4:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc bot}*
H5 : {L, hyp B |- conc bot}*
============================
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < apply IH to _ H4 with C = C.
Subgoal 4:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc bot}*
H5 : {L, hyp B |- conc bot}*
H6 : {L, hyp A |- conc C}
============================
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < apply IH to _ H5 with C = C.
Subgoal 4:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc bot}*
H5 : {L, hyp B |- conc bot}*
H6 : {L, hyp A |- conc C}
H7 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 5:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc bot}*
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < apply IH to _ H5 with C = C.
Subgoal 5:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc bot}*
H6 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 6:

Variables: L C T A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc bot}*
============================
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < apply IH to _ H4 with C = C.
Subgoal 6:

Variables: L C T A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc bot}*
H5 : {L, hyp (A T) |- conc C}
============================
 {L |- conc C}

Subgoal 7 is:
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 7:

Variables: L C A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc bot}*
============================
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < apply IH to _ H4 with C = C.
Subgoal 7:

Variables: L C A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc bot}*
H5 : {L, hyp (A n1) |- conc C}
============================
 {L |- conc C}

Subgoal 8 is:
 {L |- conc C}

bot_inv < search.
Subgoal 8:

Variables: L C F
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L, [F] |- conc bot}*
H4 : member F L
============================
 {L |- conc C}

bot_inv < apply ctx_lemma to H1 H4.
Subgoal 8:

Variables: L C A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L, [hyp A] |- conc bot}*
H4 : member (hyp A) L
============================
 {L |- conc C}

bot_inv < case H3.
Proof completed.
Abella < Theorem and_left_inv : 
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}.


============================
 forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}

and_left_inv < induction on 2.

IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
============================
 forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}@ -> {L |- conc C1}

and_left_inv < intros.

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H2 : {L |- conc (and C1 C2)}@
============================
 {L |- conc C1}

and_left_inv < case H2.
Subgoal 1:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (and C1 C2)}*
============================
 {L |- conc C1}

Subgoal 2 is:
 {L |- conc C1}

Subgoal 3 is:
 {L |- conc C1}

Subgoal 4 is:
 {L |- conc C1}

Subgoal 5 is:
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 2:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
 {L |- conc C1}

Subgoal 3 is:
 {L |- conc C1}

Subgoal 4 is:
 {L |- conc C1}

Subgoal 5 is:
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 3:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- conc C1}*
H4 : {L |- conc C2}*
============================
 {L |- conc C1}

Subgoal 4 is:
 {L |- conc C1}

Subgoal 5 is:
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
============================
 {L |- conc C1}

Subgoal 5 is:
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < apply IH to _ H4.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
H5 : {L, hyp A, hyp B |- conc C1}
============================
 {L |- conc C1}

Subgoal 5 is:
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 5:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < apply IH to _ H4.
Subgoal 5:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C1}
============================
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < apply IH to _ H5.
Subgoal 5:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C1}
H7 : {L, hyp B |- conc C1}
============================
 {L |- conc C1}

Subgoal 6 is:
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 6:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < apply IH to _ H5.
Subgoal 6:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp B |- conc C1}
============================
 {L |- conc C1}

Subgoal 7 is:
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 7:

Variables: L C1 C2 T A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
============================
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < apply IH to _ H4.
Subgoal 7:

Variables: L C1 C2 T A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
H5 : {L, hyp (A T) |- conc C1}
============================
 {L |- conc C1}

Subgoal 8 is:
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 8:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
============================
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < apply IH to _ H4.
Subgoal 8:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
H5 : {L, hyp (A n1) |- conc C1}
============================
 {L |- conc C1}

Subgoal 9 is:
 {L |- conc C1}

and_left_inv < search.
Subgoal 9:

Variables: L C1 C2 F
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L, [F] |- conc (and C1 C2)}*
H4 : member F L
============================
 {L |- conc C1}

and_left_inv < apply ctx_lemma to H1 H4.
Subgoal 9:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L, [hyp A] |- conc (and C1 C2)}*
H4 : member (hyp A) L
============================
 {L |- conc C1}

and_left_inv < case H3.
Proof completed.
Abella < Theorem and_right_inv : 
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}.


============================
 forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}

and_right_inv < induction on 2.

IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
============================
 forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}@ -> {L |- conc C2}

and_right_inv < intros.

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H2 : {L |- conc (and C1 C2)}@
============================
 {L |- conc C2}

and_right_inv < case H2.
Subgoal 1:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and C1 C2)}*
============================
 {L |- conc C2}

Subgoal 2 is:
 {L |- conc C2}

Subgoal 3 is:
 {L |- conc C2}

Subgoal 4 is:
 {L |- conc C2}

Subgoal 5 is:
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 2:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
 {L |- conc C2}

Subgoal 3 is:
 {L |- conc C2}

Subgoal 4 is:
 {L |- conc C2}

Subgoal 5 is:
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 3:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- conc C1}*
H4 : {L |- conc C2}*
============================
 {L |- conc C2}

Subgoal 4 is:
 {L |- conc C2}

Subgoal 5 is:
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
============================
 {L |- conc C2}

Subgoal 5 is:
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < apply IH to _ H4.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
H5 : {L, hyp A, hyp B |- conc C2}
============================
 {L |- conc C2}

Subgoal 5 is:
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 5:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < apply IH to _ H4.
Subgoal 5:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C2}
============================
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < apply IH to _ H5.
Subgoal 5:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C2}
H7 : {L, hyp B |- conc C2}
============================
 {L |- conc C2}

Subgoal 6 is:
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 6:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < apply IH to _ H5.
Subgoal 6:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp B |- conc C2}
============================
 {L |- conc C2}

Subgoal 7 is:
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 7:

Variables: L C1 C2 T A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
============================
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < apply IH to _ H4.
Subgoal 7:

Variables: L C1 C2 T A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
H5 : {L, hyp (A T) |- conc C2}
============================
 {L |- conc C2}

Subgoal 8 is:
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 8:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
============================
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < apply IH to _ H4.
Subgoal 8:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
H5 : {L, hyp (A n1) |- conc C2}
============================
 {L |- conc C2}

Subgoal 9 is:
 {L |- conc C2}

and_right_inv < search.
Subgoal 9:

Variables: L C1 C2 F
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L, [F] |- conc (and C1 C2)}*
H4 : member F L
============================
 {L |- conc C2}

and_right_inv < apply ctx_lemma to H1 H4.
Subgoal 9:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L, [hyp A] |- conc (and C1 C2)}*
H4 : member (hyp A) L
============================
 {L |- conc C2}

and_right_inv < case H3.
Proof completed.
Abella < Theorem imp_inv : 
forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}.


============================
 forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}

imp_inv < induction on 2.

IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
============================
 forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}@ -> {L, hyp C1 |- conc C2}

imp_inv < intros.

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H2 : {L |- conc (imp C1 C2)}@
============================
 {L, hyp C1 |- conc C2}

imp_inv < case H2.
Subgoal 1:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp C1 C2)}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 2 is:
 {L, hyp C1 |- conc C2}

Subgoal 3 is:
 {L, hyp C1 |- conc C2}

Subgoal 4 is:
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 2:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 3 is:
 {L, hyp C1 |- conc C2}

Subgoal 4 is:
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 3:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (imp C1 C2)}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 4 is:
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < apply IH to _ H4.
Subgoal 3:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (imp C1 C2)}*
H5 : {L, hyp A, hyp B, hyp C1 |- conc C2}
============================
 {L, hyp C1 |- conc C2}

Subgoal 4 is:
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (imp C1 C2)}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < apply IH to _ H4.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (imp C1 C2)}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
H6 : {L, hyp A, hyp C1 |- conc C2}
============================
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < apply IH to _ H5.
Subgoal 4:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (imp C1 C2)}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
H6 : {L, hyp A, hyp C1 |- conc C2}
H7 : {L, hyp B, hyp C1 |- conc C2}
============================
 {L, hyp C1 |- conc C2}

Subgoal 5 is:
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 5:

Variables: L C1 C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L, hyp C1 |- conc C2}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 6 is:
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 6:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < apply IH to _ H5.
Subgoal 6:

Variables: L C1 C2 B A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
H6 : {L, hyp B, hyp C1 |- conc C2}
============================
 {L, hyp C1 |- conc C2}

Subgoal 7 is:
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 7:

Variables: L C1 C2 T A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (imp C1 C2)}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < apply IH to _ H4.
Subgoal 7:

Variables: L C1 C2 T A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (imp C1 C2)}*
H5 : {L, hyp (A T), hyp C1 |- conc C2}
============================
 {L, hyp C1 |- conc C2}

Subgoal 8 is:
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 8:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (imp C1 C2)}*
============================
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < apply IH to _ H4.
Subgoal 8:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (imp C1 C2)}*
H5 : {L, hyp (A n1), hyp C1 |- conc C2}
============================
 {L, hyp C1 |- conc C2}

Subgoal 9 is:
 {L, hyp C1 |- conc C2}

imp_inv < search.
Subgoal 9:

Variables: L C1 C2 F
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L, [F] |- conc (imp C1 C2)}*
H4 : member F L
============================
 {L, hyp C1 |- conc C2}

imp_inv < apply ctx_lemma to H1 H4.
Subgoal 9:

Variables: L C1 C2 A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
       {L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L, [hyp A] |- conc (imp C1 C2)}*
H4 : member (hyp A) L
============================
 {L, hyp C1 |- conc C2}

imp_inv < case H3.
Proof completed.
Abella < Theorem all_inv : 
forall L C, ctx L -> {L |- conc (all C)} -> (nabla x, {L |- conc (C x)}).


============================
 forall L C, ctx L -> {L |- conc (all C)} -> (nabla x, {L |- conc (C x)})

all_inv < induction on 2.

IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
============================
 forall L C, ctx L -> {L |- conc (all C)}@ -> (nabla x, {L |- conc (C x)})

all_inv < intros.

Variables: L C
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H2 : {L |- conc (all C)}@
============================
 {L |- conc (C n1)}

all_inv < case H2.
Subgoal 1:

Variables: L C
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (all C)}*
============================
 {L |- conc (C n1)}

Subgoal 2 is:
 {L |- conc (C n1)}

Subgoal 3 is:
 {L |- conc (C n1)}

Subgoal 4 is:
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 2:

Variables: L C
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp bot}*
============================
 {L |- conc (C n1)}

Subgoal 3 is:
 {L |- conc (C n1)}

Subgoal 4 is:
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 3:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (all C)}*
============================
 {L |- conc (C n1)}

Subgoal 4 is:
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < apply IH to _ H4.
Subgoal 3:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (all C)}*
H5 : {L, hyp A, hyp B |- conc (C n1)}
============================
 {L |- conc (C n1)}

Subgoal 4 is:
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 4:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (all C)}*
H5 : {L, hyp B |- conc (all C)}*
============================
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < apply IH to _ H4.
Subgoal 4:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (all C)}*
H5 : {L, hyp B |- conc (all C)}*
H6 : {L, hyp A |- conc (C n1)}
============================
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < apply IH to _ H5.
Subgoal 4:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (all C)}*
H5 : {L, hyp B |- conc (all C)}*
H6 : {L, hyp A |- conc (C n1)}
H7 : {L, hyp B |- conc (C n1)}
============================
 {L |- conc (C n1)}

Subgoal 5 is:
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 5:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (all C)}*
============================
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < apply IH to _ H5.
Subgoal 5:

Variables: L C B A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (all C)}*
H6 : {L, hyp B |- conc (C n1)}
============================
 {L |- conc (C n1)}

Subgoal 6 is:
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 6:

Variables: L C
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- conc (C n1)}*
============================
 {L |- conc (C n1)}

Subgoal 7 is:
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 7:

Variables: L C T A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (all C)}*
============================
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < apply IH to _ H4.
Subgoal 7:

Variables: L C T A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (all C)}*
H5 : {L, hyp (A T) |- conc (C n1)}
============================
 {L |- conc (C n1)}

Subgoal 8 is:
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 8:

Variables: L C A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (all C)}*
============================
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < apply IH to _ H4.
Subgoal 8:

Variables: L C A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (all C)}*
H5 : {L, hyp (A n1) |- conc (C n2)}
============================
 {L |- conc (C n1)}

Subgoal 9 is:
 {L |- conc (C n1)}

all_inv < search.
Subgoal 9:

Variables: L C F
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L, [F] |- conc (all C)}*
H4 : member F L
============================
 {L |- conc (C n1)}

all_inv < apply ctx_lemma to H1 H4.
Subgoal 9:

Variables: L C A
IH : forall L C, ctx L -> {L |- conc (all C)}* ->
       (nabla x, {L |- conc (C x)})
H1 : ctx L
H3 : {L, [hyp A] |- conc (all C)}*
H4 : member (hyp A) L
============================
 {L |- conc (C n1)}

all_inv < case H3.
Proof completed.
Abella < Theorem cut_admissibility : 
forall L K C, {form K} -> ctx L -> {L |- conc K} -> {L, hyp K |- conc C} ->
  {L |- conc C}.


============================
 forall L K C, {form K} -> ctx L -> {L |- conc K} -> {L, hyp K |- conc C} ->
   {L |- conc C}

cut_admissibility < induction on 1.

IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
============================
 forall L K C, {form K}@ -> ctx L -> {L |- conc K} -> {L, hyp K |- conc C} ->
   {L |- conc C}

cut_admissibility < induction on 4.

IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
============================
 forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
   {L, hyp K |- conc C}@@ -> {L |- conc C}

cut_admissibility < intros.

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H4 : {L, hyp K |- conc C}@@
============================
 {L |- conc C}

cut_admissibility < case H4.
Subgoal 1:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp C}**
============================
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 1:

Variables: L K C F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [F] |- hyp C}**
H7 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H7.
Subgoal 1.1:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [hyp K] |- hyp C}**
============================
 {L |- conc C}

Subgoal 1.2 is:
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H6.
Subgoal 1.1:

Variables: L C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form C}@
H2 : ctx L
H3 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 1.2 is:
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 1.2:

Variables: L K C F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [F] |- hyp C}**
H8 : member F L
============================
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H8.
Subgoal 1.2:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [hyp A] |- hyp C}**
H8 : member (hyp A) L
============================
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H6.
Subgoal 1.2:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H8 : member (hyp C) L
============================
 {L |- conc C}

Subgoal 2 is:
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 2:

Variables: L K
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
============================
 {L |- conc top}

Subgoal 3 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 3:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp bot}**
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 3:

Variables: L K C F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [F] |- hyp bot}**
H7 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H7.
Subgoal 3.1:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [hyp K] |- hyp bot}**
============================
 {L |- conc C}

Subgoal 3.2 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H6.
Subgoal 3.1:

Variables: L C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form bot}@
H2 : ctx L
H3 : {L |- conc bot}
============================
 {L |- conc C}

Subgoal 3.2 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply bot_inv to H2 H3 with C = C.
Subgoal 3.1:

Variables: L C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form bot}@
H2 : ctx L
H3 : {L |- conc bot}
H8 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 3.2 is:
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 3.2:

Variables: L K C F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [F] |- hyp bot}**
H8 : member F L
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H8.
Subgoal 3.2:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, [hyp A] |- hyp bot}**
H8 : member (hyp A) L
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H6.
Subgoal 3.2:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H8 : member (hyp bot) L
============================
 {L |- conc C}

Subgoal 4 is:
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 4:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L, hyp K |- conc B}**
============================
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H5.
Subgoal 4:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L, hyp K |- conc B}**
H7 : {L |- conc A}
============================
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 4:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L, hyp K |- conc B}**
H7 : {L |- conc A}
H8 : {L |- conc B}
============================
 {L |- conc (and A B)}

Subgoal 5 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 5:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (and A B)}**
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 5:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (and A B)}**
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 5:

Variables: L K C B A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H8 : {L, hyp K, [F] |- hyp (and A B)}**
H9 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H9.
Subgoal 5.1:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H8 : {L, hyp K, [hyp K] |- hyp (and A B)}**
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H8.
Subgoal 5.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (and A B)}@
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply and_left_inv to _ H3.
Subgoal 5.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (and A B)}@
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H10 : {L |- conc A}
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply and_right_inv to _ H3.
Subgoal 5.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (and A B)}@
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H10 : {L |- conc A}
H11 : {L |- conc B}
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H1.
Subgoal 5.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H10 : {L |- conc A}
H11 : {L |- conc B}
H12 : {form A}*
H13 : {form B}*
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H12 _ H10 H7.
Subgoal 5.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H10 : {L |- conc A}
H11 : {L |- conc B}
H12 : {form A}*
H13 : {form B}*
H14 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H13 _ H11 H14.
Subgoal 5.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H10 : {L |- conc A}
H11 : {L |- conc B}
H12 : {form A}*
H13 : {form B}*
H14 : {L, hyp B |- conc C}
H15 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 5.2 is:
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 5.2:

Variables: L K C B A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H8 : {L, hyp K, [F] |- hyp (and A B)}**
H10 : member F L
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H10.
Subgoal 5.2:

Variables: L K C B A A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H8 : {L, hyp K, [hyp A1] |- hyp (and A B)}**
H10 : member (hyp A1) L
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H8.
Subgoal 5.2:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H10 : member (hyp (and A B)) L
============================
 {L |- conc C}

Subgoal 6 is:
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 6:

Variables: L K A B
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
============================
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 H2 H3 H5.
Subgoal 6:

Variables: L K A B
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L |- conc A}
============================
 {L |- conc (or A B)}

Subgoal 7 is:
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 7:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc B}**
============================
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 H2 H3 H5.
Subgoal 7:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc B}**
H6 : {L |- conc B}
============================
 {L |- conc (or A B)}

Subgoal 8 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (or A B)}**
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 8:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (or A B)}**
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H7.
Subgoal 8:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (or A B)}**
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 8:

Variables: L K C B A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [F] |- hyp (or A B)}**
H11 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H11.
Subgoal 8.1:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [hyp K] |- hyp (or A B)}**
============================
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H10.
Subgoal 8.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < assert forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
  {L, hyp B |- conc D} -> {L |- conc D}.
Subgoal 8.1.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
============================
 forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
   {L, hyp B |- conc D} -> {L |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < induction on 2.
Subgoal 8.1.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
============================
 forall L D, ctx L -> {L |- conc (or A B)}@@@ -> {L, hyp A |- conc D} ->
   {L, hyp B |- conc D} -> {L |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < intros.
Subgoal 8.1.1:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H13 : {L1 |- conc (or A B)}@@@
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H13.
Subgoal 8.1.1.1:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (or A B)}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.2 is:
 {L1 |- conc D}

Subgoal 8.1.1.3 is:
 {L1 |- conc D}

Subgoal 8.1.1.4 is:
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.2:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp bot}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.3 is:
 {L1 |- conc D}

Subgoal 8.1.1.4 is:
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.3:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (and A1 B1)}***
H17 : {L1, hyp A1, hyp B1 |- conc (or A B)}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.4 is:
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H17 H14 H15.
Subgoal 8.1.1.3:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (and A1 B1)}***
H17 : {L1, hyp A1, hyp B1 |- conc (or A B)}***
H18 : {L1, hyp A1, hyp B1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.4 is:
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.4:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- conc A}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H1.
Subgoal 8.1.1.4:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- conc A}***
H17 : {form A}*
H18 : {form B}*
============================
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H17 H12 H16 H14.
Subgoal 8.1.1.4:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- conc A}***
H17 : {form A}*
H18 : {form B}*
H19 : {L1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.5 is:
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.5:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- conc B}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H1.
Subgoal 8.1.1.5:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- conc B}***
H17 : {form A}*
H18 : {form B}*
============================
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H18 H12 H16 H15.
Subgoal 8.1.1.5:

Variables: L C B A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- conc B}***
H17 : {form A}*
H18 : {form B}*
H19 : {L1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.6 is:
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.6:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (or A1 B1)}***
H17 : {L1, hyp A1 |- conc (or A B)}***
H18 : {L1, hyp B1 |- conc (or A B)}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H17 H14 H15.
Subgoal 8.1.1.6:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (or A1 B1)}***
H17 : {L1, hyp A1 |- conc (or A B)}***
H18 : {L1, hyp B1 |- conc (or A B)}***
H19 : {L1, hyp A1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H18 H14 H15.
Subgoal 8.1.1.6:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (or A1 B1)}***
H17 : {L1, hyp A1 |- conc (or A B)}***
H18 : {L1, hyp B1 |- conc (or A B)}***
H19 : {L1, hyp A1 |- conc D}
H20 : {L1, hyp B1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.7 is:
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.7:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (imp A1 B1)}***
H17 : {L1 |- conc A1}***
H18 : {L1, hyp B1 |- conc (or A B)}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H18 H14 H15.
Subgoal 8.1.1.7:

Variables: L C B A L1 D B1 A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (imp A1 B1)}***
H17 : {L1 |- conc A1}***
H18 : {L1, hyp B1 |- conc (or A B)}***
H19 : {L1, hyp B1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.8 is:
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.8:

Variables: L C B A L1 D T A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (all A1)}***
H17 : {L1, hyp (A1 T) |- conc (or A B)}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H17 H14 H15.
Subgoal 8.1.1.8:

Variables: L C B A L1 D T A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (all A1)}***
H17 : {L1, hyp (A1 T) |- conc (or A B)}***
H18 : {L1, hyp (A1 T) |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.9 is:
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.9:

Variables: L C B A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (ex A1)}***
H17 : {L1, hyp (A1 n1) |- conc (or A B)}***
============================
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H17 H14 H15.
Subgoal 8.1.1.9:

Variables: L C B A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1 |- hyp (ex A1)}***
H17 : {L1, hyp (A1 n1) |- conc (or A B)}***
H18 : {L1, hyp (A1 n1) |- conc D}
============================
 {L1 |- conc D}

Subgoal 8.1.1.10 is:
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.1.1.10:

Variables: L C B A L1 D F1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1, [F1] |- conc (or A B)}***
H17 : member F1 L1
============================
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H12 H17.
Subgoal 8.1.1.10:

Variables: L C B A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H12 : ctx L1
H14 : {L1, hyp A |- conc D}
H15 : {L1, hyp B |- conc D}
H16 : {L1, [hyp A1] |- conc (or A B)}***
H17 : member (hyp A1) L1
============================
 {L1 |- conc D}

Subgoal 8.1 is:
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H16.
Subgoal 8.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H12 : forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
============================
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply H12 to H2 H3 H8 H9.
Subgoal 8.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H12 : forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
        {L, hyp B |- conc D} -> {L |- conc D}
H13 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 8.2 is:
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 8.2:

Variables: L K C B A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [F] |- hyp (or A B)}**
H12 : member F L
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H12.
Subgoal 8.2:

Variables: L K C B A A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [hyp A1] |- hyp (or A B)}**
H12 : member (hyp A1) L
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H10.
Subgoal 8.2:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H12 : member (hyp (or A B)) L
============================
 {L |- conc C}

Subgoal 9 is:
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 9:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, hyp A |- conc B}**
============================
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H5.
Subgoal 9:

Variables: L K B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, hyp A |- conc B}**
H6 : {L, hyp A |- conc B}
============================
 {L |- conc (imp A B)}

Subgoal 10 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 10:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (imp A B)}**
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 10:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (imp A B)}**
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H7.
Subgoal 10:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (imp A B)}**
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 10:

Variables: L K C B A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [F] |- hyp (imp A B)}**
H11 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H11.
Subgoal 10.1:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [hyp K] |- hyp (imp A B)}**
============================
 {L |- conc C}

Subgoal 10.2 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H10.
Subgoal 10.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (imp A B)}@
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
============================
 {L |- conc C}

Subgoal 10.2 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply imp_inv to _ H3.
Subgoal 10.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (imp A B)}@
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H12 : {L, hyp A |- conc B}
============================
 {L |- conc C}

Subgoal 10.2 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H1.
Subgoal 10.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H12 : {L, hyp A |- conc B}
H13 : {form A}*
H14 : {form B}*
============================
 {L |- conc C}

Subgoal 10.2 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H13 _ H8 H12.
Subgoal 10.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H12 : {L, hyp A |- conc B}
H13 : {form A}*
H14 : {form B}*
H15 : {L |- conc B}
============================
 {L |- conc C}

Subgoal 10.2 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H14 _ H15 H9.
Subgoal 10.1:

Variables: L C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H12 : {L, hyp A |- conc B}
H13 : {form A}*
H14 : {form B}*
H15 : {L |- conc B}
H16 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 10.2 is:
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 10.2:

Variables: L K C B A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [F] |- hyp (imp A B)}**
H12 : member F L
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H12.
Subgoal 10.2:

Variables: L K C B A A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H10 : {L, hyp K, [hyp A1] |- hyp (imp A B)}**
H12 : member (hyp A1) L
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H10.
Subgoal 10.2:

Variables: L K C B A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H12 : member (hyp (imp A B)) L
============================
 {L |- conc C}

Subgoal 11 is:
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 11:

Variables: L K A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A n1)}**
============================
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H5.
Subgoal 11:

Variables: L K A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A n1)}**
H6 : {L |- conc (A n1)}
============================
 {L |- conc (all A)}

Subgoal 12 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 12:

Variables: L K C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (all A)}**
H6 : {L, hyp K, hyp (A T) |- conc C}**
============================
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 12:

Variables: L K C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (all A)}**
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
============================
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 12:

Variables: L K C T A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H8 : {L, hyp K, [F] |- hyp (all A)}**
H9 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H9.
Subgoal 12.1:

Variables: L K C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H8 : {L, hyp K, [hyp K] |- hyp (all A)}**
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H8.
Subgoal 12.1:

Variables: L C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (all A)}@
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply all_inv to _ H3.
Subgoal 12.1:

Variables: L C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (all A)}@
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H10 : {L |- conc (A n1)}
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H1.
Subgoal 12.1:

Variables: L C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H10 : {L |- conc (A n1)}
H11 : {form (A n1)}*
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility <  inst H10 with n1 = T.
Subgoal 12.1:

Variables: L C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H10 : {L |- conc (A n1)}
H11 : {form (A n1)}*
H12 : {L |- conc (A T)}
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility <  inst H11 with n1 = T.
Subgoal 12.1:

Variables: L C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H10 : {L |- conc (A n1)}
H11 : {form (A n1)}*
H12 : {L |- conc (A T)}
H13 : {form (A T)}*
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H13 _ H12 H7.
Subgoal 12.1:

Variables: L C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H10 : {L |- conc (A n1)}
H11 : {form (A n1)}*
H12 : {L |- conc (A T)}
H13 : {form (A T)}*
H14 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 12.2 is:
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 12.2:

Variables: L K C T A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H8 : {L, hyp K, [F] |- hyp (all A)}**
H10 : member F L
============================
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H10.
Subgoal 12.2:

Variables: L K C T A A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H8 : {L, hyp K, [hyp A1] |- hyp (all A)}**
H10 : member (hyp A1) L
============================
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H8.
Subgoal 12.2:

Variables: L K C T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H10 : member (hyp (all A)) L
============================
 {L |- conc C}

Subgoal 13 is:
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 13:

Variables: L K T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A T)}**
============================
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 H2 H3 H5.
Subgoal 13:

Variables: L K T A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A T)}**
H6 : {L |- conc (A T)}
============================
 {L |- conc (ex A)}

Subgoal 14 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (ex A)}**
H6 : {L, hyp K, hyp (A n1) |- conc C}**
============================
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 14:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (ex A)}**
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
============================
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 14:

Variables: L K C A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H8 : {L, hyp K, [F] |- hyp (ex A)}**
H9 : member F (hyp K :: L)
============================
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H9.
Subgoal 14.1:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H8 : {L, hyp K, [hyp K] |- hyp (ex A)}**
============================
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H8.
Subgoal 14.1:

Variables: L C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
============================
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < assert forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
  {L, hyp (A x) |- conc D} -> {L |- conc D}.
Subgoal 14.1.1:

Variables: L C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
============================
 forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
   {L, hyp (A x) |- conc D} -> {L |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < induction on 2.
Subgoal 14.1.1:

Variables: L C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
============================
 forall L D, nabla x, ctx L -> {L |- conc (ex A)}@@@ ->
   {L, hyp (A x) |- conc D} -> {L |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < intros.
Subgoal 14.1.1:

Variables: L C A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H11 : {L1 |- conc (ex A)}@@@
H12 : {L1, hyp (A n1) |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H11.
Subgoal 14.1.1.1:

Variables: L C A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (ex A)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.2 is:
 {L1 |- conc D}

Subgoal 14.1.1.3 is:
 {L1 |- conc D}

Subgoal 14.1.1.4 is:
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.2:

Variables: L C A L1 D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp bot}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.3 is:
 {L1 |- conc D}

Subgoal 14.1.1.4 is:
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.3:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (and A1 B)}***
H14 : {L1, hyp A1, hyp B |- conc (ex A)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.4 is:
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H14 H12.
Subgoal 14.1.1.3:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (and A1 B)}***
H14 : {L1, hyp A1, hyp B |- conc (ex A)}***
H15 : {L1, hyp A1, hyp B |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.4 is:
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.4:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (or A1 B)}***
H14 : {L1, hyp A1 |- conc (ex A)}***
H15 : {L1, hyp B |- conc (ex A)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H14 H12.
Subgoal 14.1.1.4:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (or A1 B)}***
H14 : {L1, hyp A1 |- conc (ex A)}***
H15 : {L1, hyp B |- conc (ex A)}***
H16 : {L1, hyp A1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H15 H12.
Subgoal 14.1.1.4:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (or A1 B)}***
H14 : {L1, hyp A1 |- conc (ex A)}***
H15 : {L1, hyp B |- conc (ex A)}***
H16 : {L1, hyp A1 |- conc D}
H17 : {L1, hyp B |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.5 is:
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.5:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (imp A1 B)}***
H14 : {L1 |- conc A1}***
H15 : {L1, hyp B |- conc (ex A)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H15 H12.
Subgoal 14.1.1.5:

Variables: L C A L1 D B A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (imp A1 B)}***
H14 : {L1 |- conc A1}***
H15 : {L1, hyp B |- conc (ex A)}***
H16 : {L1, hyp B |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.6 is:
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.6:

Variables: L C A L1 D T A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (all A1)}***
H14 : {L1, hyp (A1 T) |- conc (ex A)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H14 H12.
Subgoal 14.1.1.6:

Variables: L C A L1 D T A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (all A1)}***
H14 : {L1, hyp (A1 T) |- conc (ex A)}***
H15 : {L1, hyp (A1 T) |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.7 is:
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.7:

Variables: L C A L1 D T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- conc (A T)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H1.
Subgoal 14.1.1.7:

Variables: L C A L1 D T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- conc (A T)}***
H14 : {form (A n1)}*
============================
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility <  inst H14 with n1 = T.
Subgoal 14.1.1.7:

Variables: L C A L1 D T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- conc (A T)}***
H14 : {form (A n1)}*
H15 : {form (A T)}*
============================
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility <  inst H12 with n1 = T.
Subgoal 14.1.1.7:

Variables: L C A L1 D T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- conc (A T)}***
H14 : {form (A n1)}*
H15 : {form (A T)}*
H16 : {L1, hyp (A T) |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH to H15 H10 H13 H16.
Subgoal 14.1.1.7:

Variables: L C A L1 D T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- conc (A T)}***
H14 : {form (A n1)}*
H15 : {form (A T)}*
H16 : {L1, hyp (A T) |- conc D}
H17 : {L1 |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.8 is:
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.8:

Variables: L C A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (ex A1)}***
H14 : {L1, hyp (A1 n1) |- conc (ex A)}***
============================
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < assert {L1, hyp (A n2) |- conc D}.
Subgoal 14.1.1.8:

Variables: L C A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (ex A1)}***
H14 : {L1, hyp (A1 n1) |- conc (ex A)}***
H15 : {L1, hyp (A n2) |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply IH2 to _ H14 H15.
Subgoal 14.1.1.8:

Variables: L C A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1 |- hyp (ex A1)}***
H14 : {L1, hyp (A1 n1) |- conc (ex A)}***
H15 : {L1, hyp (A n2) |- conc D}
H16 : {L1, hyp (A1 n1) |- conc D}
============================
 {L1 |- conc D}

Subgoal 14.1.1.9 is:
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.1.1.9:

Variables: L C A L1 D F1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1, [F1] |- conc (ex A)}***
H14 : member F1 L1
============================
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H10 H14.
Subgoal 14.1.1.9:

Variables: L C A L1 D A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : ctx L1
H12 : {L1, hyp (A n1) |- conc D}
H13 : {L1, [hyp A1] |- conc (ex A)}***
H14 : member (hyp A1) L1
============================
 {L1 |- conc D}

Subgoal 14.1 is:
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H13.
Subgoal 14.1:

Variables: L C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H10 : forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
============================
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply H10 to H2 H3 H7.
Subgoal 14.1:

Variables: L C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H10 : forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
        {L, hyp (A x) |- conc D} -> {L |- conc D}
H11 : {L |- conc C}
============================
 {L |- conc C}

Subgoal 14.2 is:
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 14.2:

Variables: L K C A F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H8 : {L, hyp K, [F] |- hyp (ex A)}**
H10 : member F L
============================
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H10.
Subgoal 14.2:

Variables: L K C A A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H8 : {L, hyp K, [hyp A1] |- hyp (ex A)}**
H10 : member (hyp A1) L
============================
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < case H8.
Subgoal 14.2:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H10 : member (hyp (ex A)) L
============================
 {L |- conc C}

Subgoal 15 is:
 {L |- conc C}

cut_admissibility < search.
Subgoal 15:

Variables: L K C F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, [F] |- conc C}**
H6 : member F (hyp K :: L)
============================
 {L |- conc C}

cut_admissibility < case H6.
Subgoal 15.1:

Variables: L K C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, [hyp K] |- conc C}**
============================
 {L |- conc C}

Subgoal 15.2 is:
 {L |- conc C}

cut_admissibility < case H5.
Subgoal 15.2:

Variables: L K C F
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, [F] |- conc C}**
H7 : member F L
============================
 {L |- conc C}

cut_admissibility < apply ctx_lemma to H2 H7.
Subgoal 15.2:

Variables: L K C A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
       {L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
        {L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, [hyp A] |- conc C}**
H7 : member (hyp A) L
============================
 {L |- conc C}

cut_admissibility < case H5.
Proof completed.
Abella <