Welcome to Abella 2.0.1-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, L
  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, L, 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: E, L, 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, L, 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: E, L, 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, F, 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, F, 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, F, 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, F, 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, F, 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, 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 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, 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 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, F, 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, F, 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}
  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, 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}
  ============================
   {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, 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 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, 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 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, 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 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, F, 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, F, 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}
  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, 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 |- 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, 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 |- 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, 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 |- 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, 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, [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, 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 (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, 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 (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, 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 (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, 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}
  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, 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}
  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, 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}
  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, F, 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, F, 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}
  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, C, 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, C, 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, 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 |- 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, 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 |- 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, 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, [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, 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 (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, 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 (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, 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 (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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, 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, K, C, B, A, F, L1, D, F1, 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, 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 (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, 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 (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, F, 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, F, 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}
  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, 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 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, 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 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, 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, [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, 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 (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, 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 (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, 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}
  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, 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}
  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, 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}
  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, F, 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, F, 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}
  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, 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 |- 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, 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 |- 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, 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, [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, 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 (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, 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 (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, 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}
  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, 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}
  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, 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}
  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, 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}
  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, F, 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, F, 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}
  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, 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 |- 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, 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 |- 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, 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, [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, 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 (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, 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 (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, 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 (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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, 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, K, C, A, F, L1, D, F1, 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, 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 (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, 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 (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, F, 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, F, 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}
  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, 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, [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, F, 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 < Goodbye.