Welcome to Abella 2.0.2-parinati
Abella < Specification "impcut.elf".
Reading specification "impcut.elf"
sig impcut.
  type i lftype.
  type form lftype.
  type imp lfobj -> lfobj -> lfobj.
  type atom lfobj -> lfobj.
  type hyp lfobj -> lftype.
  type conc lfobj -> lftype.
  type init lfobj -> lfobj -> lfobj.
  type impR lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj.
  type impL lfobj -> lfobj -> lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj -> lfobj.
end.
module impcut.
  (* i:type *)
  lfisty i.
  (* form:type *)
  lfisty form.
  (* imp:form -> form -> form *)
  pi lf_1\lfhas lf_1 form =>
    pi lf_2\lfhas lf_2 form => lfhas (imp lf_1 lf_2) form.
  (* atom:i -> form *)
  pi lf_1\lfhas lf_1 i => lfhas (atom lf_1) form.
  (* hyp:form -> type *)
  pi lf_1\lfhas lf_1 form => lfisty (hyp lf_1).
  (* conc:form -> type *)
  pi lf_1\lfhas lf_1 form => lfisty (conc lf_1).
  (* init:({P:i} hyp (atom P) -> conc (atom P)) *)
  pi P\lfhas P i =>
    pi lf_1\lfhas lf_1 (hyp (atom P)) => lfhas (init P lf_1) (conc (atom P)).
  (* impR:({A:form} {B:form} (hyp A -> conc B) -> conc (imp A B)) *)
  pi A\lfhas A form =>
    pi B\lfhas B form =>
      pi lf_1\(pi lf_2\lfhas lf_2 (hyp A) => lfhas (lf_1 lf_2) (conc B)) =>
        lfhas (impR A B lf_1) (conc (imp A B)).
  (* impL:
       ({A:form} {B:form} {C:form} conc A -> (hyp B -> conc C) ->
          hyp (imp A B) -> conc C) *)
  pi A\lfhas A form =>
    pi B\lfhas B form =>
      pi C\lfhas C form =>
        pi lf_1\lfhas lf_1 (conc A) =>
          pi lf_2\(pi lf_3\lfhas lf_3 (hyp B) => lfhas (lf_2 lf_3) (conc C)) =>
            pi lf_3\lfhas lf_3 (hyp (imp A B)) =>
              lfhas (impL A B C lf_1 lf_2 lf_3) (conc C).
end.
Abella < Define ctx : olist -> prop by 
ctx nil;
nabla p, ctx (<p:hyp A> :: G) := ctx G.
Abella < Define name : lfobj -> prop by 
nabla x, name x.
Abella < Define fresh : lfobj -> lfobj -> prop by 
nabla x, fresh x A.
Abella < Theorem prune : 
forall G E, (nabla n, member (E n) G -> (exists F, E = x\F)).

============================
 forall G E, (nabla n, member (E n) G -> (exists F, E = x\F))

prune < induction on 1.

IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
============================
 forall G E, (nabla n, member (E n) G @ -> (exists F, E = x\F))

prune < intros.

Variables: G E
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
H1 : member (E n1) G @
============================
 exists F, E = x\F

prune < case H1.
Subgoal 1:

Variables: G2 G1
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
============================
 exists F, z1\G1 = x\F

Subgoal 2 is:
 exists F, E = x\F

prune < search.
Subgoal 2:

Variables: E G2 G1
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
H2 : member (E n1) G2 *
============================
 exists F, E = x\F

prune < apply IH to H2.
Subgoal 2:

Variables: G2 G1 F
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
H2 : member F G2 *
============================
 exists F1, z1\F = x\F1

prune < search.
Proof completed.
Abella < Theorem ctx_mem : 
forall G E, ctx G -> member E G -> (exists A P, E = <P:hyp A> /\ fresh P A).

============================
 forall G E, ctx G -> member E G -> (exists A P, E = <P:hyp A> /\ fresh P A)

ctx_mem < induction on 1.

IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
============================
 forall G E, ctx G @ -> member E G ->
   (exists A P, E = <P:hyp A> /\ fresh P A)

ctx_mem < intros.

Variables: G E
IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
H1 : ctx G @
H2 : member E G
============================
 exists A P, E = <P:hyp A> /\ fresh P A

ctx_mem < case H1.
Subgoal 1:

Variables: E
IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
H2 : member E nil
============================
 exists A P, E = <P:hyp A> /\ fresh P A

Subgoal 2 is:
 exists A P, E n1 = <P:hyp A> /\ fresh P A

ctx_mem < case H2.
Subgoal 2:

Variables: E G1 A
IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
H2 : member (E n1) (<n1:hyp A> :: G1)
H3 : ctx G1 *
============================
 exists A P, E n1 = <P:hyp A> /\ fresh P A

ctx_mem < case H2.
Subgoal 2.1:

Variables: G1 A
IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
H3 : ctx G1 *
============================
 exists A1 P, <n1:hyp A> = <P:hyp A1> /\ fresh P A1

Subgoal 2.2 is:
 exists A P, E n1 = <P:hyp A> /\ fresh P A

ctx_mem < search.
Subgoal 2.2:

Variables: E G1 A
IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
H3 : ctx G1 *
H4 : member (E n1) G1
============================
 exists A P, E n1 = <P:hyp A> /\ fresh P A

ctx_mem < apply IH to H3 H4.
Subgoal 2.2:

Variables: G1 A A1 P
IH : forall G E, ctx G * -> member E G ->
       (exists A P, E = <P:hyp A> /\ fresh P A)
H3 : ctx G1 *
H4 : member <P n1:hyp (A1 n1)> G1
H5 : fresh (P n1) (A1 n1)
============================
 exists A P1, <P n1:hyp (A1 n1)> = <P1:hyp A> /\ fresh P1 A

ctx_mem < search.
Proof completed.
Abella < Theorem strength_i : 
forall G U, ctx G -> <G |- U:i> -> <U:i>.

============================
 forall G U, ctx G -> <G |- U:i> -> <U:i>

strength_i < induction on 2.

IH : forall G U, ctx G -> <G |- U:i>* -> <U:i>
============================
 forall G U, ctx G -> <G |- U:i>@ -> <U:i>

strength_i < intros.

Variables: G U
IH : forall G U, ctx G -> <G |- U:i>* -> <U:i>
H1 : ctx G
H2 : <G |- U:i>@
============================
 <U:i>

strength_i < case H2.

Variables: G U F
IH : forall G U, ctx G -> <G |- U:i>* -> <U:i>
H1 : ctx G
H3 : <G, [F] |- U:i>*
H4 : member F G
============================
 <U:i>

strength_i < apply ctx_mem to H1 H4.

Variables: G U A P
IH : forall G U, ctx G -> <G |- U:i>* -> <U:i>
H1 : ctx G
H3 : <G, [P:hyp A] |- U:i>*
H4 : member <P:hyp A> G
H5 : fresh P A
============================
 <U:i>

strength_i < case H3.
Proof completed.
Abella < Theorem strength_form : 
forall G F, ctx G -> <G |- F:form> -> <F:form>.

============================
 forall G F, ctx G -> <G |- F:form> -> <F:form>

strength_form < induction on 2.

IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
============================
 forall G F, ctx G -> <G |- F:form>@ -> <F:form>

strength_form < intros.

Variables: G F
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- F:form>@
============================
 <F:form>

strength_form < case H2 (keep).
Subgoal 1:

Variables: G lf_2 lf_1
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- imp lf_1 lf_2:form>@
H3 : <G |- lf_1:form>*
H4 : <G |- lf_2:form>*
============================
 <imp lf_1 lf_2:form>

Subgoal 2 is:
 <atom lf_1:form>

Subgoal 3 is:
 <F:form>

strength_form < apply IH to H1 H3.
Subgoal 1:

Variables: G lf_2 lf_1
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- imp lf_1 lf_2:form>@
H3 : <G |- lf_1:form>*
H4 : <G |- lf_2:form>*
H5 : <lf_1:form>
============================
 <imp lf_1 lf_2:form>

Subgoal 2 is:
 <atom lf_1:form>

Subgoal 3 is:
 <F:form>

strength_form < apply IH to H1 H4.
Subgoal 1:

Variables: G lf_2 lf_1
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- imp lf_1 lf_2:form>@
H3 : <G |- lf_1:form>*
H4 : <G |- lf_2:form>*
H5 : <lf_1:form>
H6 : <lf_2:form>
============================
 <imp lf_1 lf_2:form>

Subgoal 2 is:
 <atom lf_1:form>

Subgoal 3 is:
 <F:form>

strength_form < search.
Subgoal 2:

Variables: G lf_1
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- atom lf_1:form>@
H3 : <G |- lf_1:i>*
============================
 <atom lf_1:form>

Subgoal 3 is:
 <F:form>

strength_form < apply strength_i to H1 H3.
Subgoal 2:

Variables: G lf_1
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- atom lf_1:form>@
H3 : <G |- lf_1:i>*
H4 : <lf_1:i>
============================
 <atom lf_1:form>

Subgoal 3 is:
 <F:form>

strength_form < search.
Subgoal 3:

Variables: G F F1
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- F:form>@
H3 : <G, [F1] |- F:form>*
H4 : member F1 G
============================
 <F:form>

strength_form < apply ctx_mem to H1 H4.
Subgoal 3:

Variables: G F A P
IH : forall G F, ctx G -> <G |- F:form>* -> <F:form>
H1 : ctx G
H2 : <G |- F:form>@
H3 : <G, [P:hyp A] |- F:form>*
H4 : member <P:hyp A> G
H5 : fresh P A
============================
 <F:form>

strength_form < case H3.
Proof completed.
Abella < Theorem prune_form : 
forall F, (nabla x, <F x:form> -> (exists FF, F = x\FF)).

============================
 forall F, (nabla x, <F x:form> -> (exists FF, F = x\FF))

prune_form < induction on 1.

IH : forall F, (nabla x, <F x:form>* -> (exists FF, F = x\FF))
============================
 forall F, (nabla x, <F x:form>@ -> (exists FF, F = x\FF))

prune_form < intros.

Variables: F
IH : forall F, (nabla x, <F x:form>* -> (exists FF, F = x\FF))
H1 : <F n1:form>@
============================
 exists FF, F = x\FF

prune_form < case H1.
Subgoal 1:

Variables: lf_2 lf_1
IH : forall F, (nabla x, <F x:form>* -> (exists FF, F = x\FF))
H2 : <lf_1 n1:form>*
H3 : <lf_2 n1:form>*
============================
 exists FF, z1\imp (lf_1 z1) (lf_2 z1) = x\FF

Subgoal 2 is:
 exists FF, z1\atom (lf_1 z1) = x\FF

prune_form < apply IH to H2.
Subgoal 1:

Variables: lf_2 FF
IH : forall F, (nabla x, <F x:form>* -> (exists FF, F = x\FF))
H2 : <FF:form>*
H3 : <lf_2 n1:form>*
============================
 exists FF1, z1\imp FF (lf_2 z1) = x\FF1

Subgoal 2 is:
 exists FF, z1\atom (lf_1 z1) = x\FF

prune_form < apply IH to H3.
Subgoal 1:

Variables: FF FF1
IH : forall F, (nabla x, <F x:form>* -> (exists FF, F = x\FF))
H2 : <FF:form>*
H3 : <FF1:form>*
============================
 exists FF2, z1\imp FF FF1 = x\FF2

Subgoal 2 is:
 exists FF, z1\atom (lf_1 z1) = x\FF

prune_form < search.
Subgoal 2:

Variables: lf_1
IH : forall F, (nabla x, <F x:form>* -> (exists FF, F = x\FF))
H2 : <lf_1 n1:i>*
============================
 exists FF, z1\atom (lf_1 z1) = x\FF

prune_form < case H2.
Proof completed.
Abella < Theorem imp_invert : 
forall G A B DD, ctx G -> <G |- DD:conc (imp A B)> ->
  (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>)).

============================
 forall G A B DD, ctx G -> <G |- DD:conc (imp A B)> ->
   (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))

imp_invert < induction on 2.

IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
============================
 forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>@ ->
   (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))

imp_invert < intros.

Variables: G A B DD
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- DD:conc (imp A B)>@
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < case H2 (keep).
Subgoal 1:

Variables: G A B lf_1
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impR A B lf_1:conc (imp A B)>@
H3 : <G |- A:form>*
H4 : <G |- B:form>*
H5 : <G, n1:hyp A |- lf_1 n1:conc B>*
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 2 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < search.
Subgoal 2:

Variables: G A B B1 A1 lf_3 lf_2 lf_1
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H5 : <G |- imp A B:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < apply IH to _ H7.
Subgoal 2:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H5 : <G |- imp A B:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < case H5.
Subgoal 2.1:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
H10 : <G |- A:form>*
H11 : <G |- B:form>*
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 2.2 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < assert <G, n2:hyp A, n1:hyp (imp A1 B1) |- impL A1 B1 B lf_1 (EE n2) lf_3:conc B>.
Subgoal 2.1:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
H10 : <G |- A:form>*
H11 : <G |- B:form>*
H12 : <G, n2:hyp A, n1:hyp (imp A1 B1) |- impL A1 B1 B lf_1 (EE n2) lf_3:
         conc B>
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 2.2 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < inst H12 with n1 = lf_3.
Subgoal 2.1:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
H10 : <G |- A:form>*
H11 : <G |- B:form>*
H12 : <G, n2:hyp A, n1:hyp (imp A1 B1) |- impL A1 B1 B lf_1 (EE n2) lf_3:
         conc B>
H13 : <G, n2:hyp A, lf_3:hyp (imp A1 B1) |- impL A1 B1 B lf_1 (EE n2) lf_3:
         conc B>
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 2.2 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < cut H13 with H8.
Subgoal 2.1:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
H10 : <G |- A:form>*
H11 : <G |- B:form>*
H12 : <G, n2:hyp A, n1:hyp (imp A1 B1) |- impL A1 B1 B lf_1 (EE n2) lf_3:
         conc B>
H13 : <G, n2:hyp A, lf_3:hyp (imp A1 B1) |- impL A1 B1 B lf_1 (EE n2) lf_3:
         conc B>
H14 : <G, n2:hyp A |- impL A1 B1 B lf_1 (EE n2) lf_3:conc B>
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 2.2 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < search.
Subgoal 2.2:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE F
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
H10 : <G, [F] |- imp A B:form>*
H11 : member F G
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < apply ctx_mem to H1 H11.
Subgoal 2.2:

Variables: G A B B1 A1 lf_3 lf_2 lf_1 EE A2 P
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- impL A1 B1 (imp A B) lf_1 lf_2 lf_3:conc (imp A B)>@
H3 : <G |- A1:form>*
H4 : <G |- B1:form>*
H6 : <G |- lf_1:conc A1>*
H7 : <G, n1:hyp B1 |- lf_2 n1:conc (imp A B)>*
H8 : <G |- lf_3:hyp (imp A1 B1)>*
H9 : <G, n1:hyp B1, n2:hyp A |- EE n2 n1:conc B>
H10 : <G, [P:hyp A2] |- imp A B:form>*
H11 : member <P:hyp A2> G
H12 : fresh P A2
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

Subgoal 3 is:
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < case H10.
Subgoal 3:

Variables: G A B DD F
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- DD:conc (imp A B)>@
H3 : <G, [F] |- DD:conc (imp A B)>*
H4 : member F G
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < apply ctx_mem to H1 H4.
Subgoal 3:

Variables: G A B DD A1 P
IH : forall G A B DD, ctx G -> <G |- DD:conc (imp A B)>* ->
       (nabla x, (exists EE, <G, x:hyp A |- EE:conc B>))
H1 : ctx G
H2 : <G |- DD:conc (imp A B)>@
H3 : <G, [P:hyp A1] |- DD:conc (imp A B)>*
H4 : member <P:hyp A1> G
H5 : fresh P A1
============================
 exists EE, <G, n1:hyp A |- EE:conc B>

imp_invert < case H3.
Proof completed.
Abella < Theorem cut_admit : 
forall G A C D1 D2,
  (nabla x, ctx G -> <A:form> -> <G |- D1:conc A> ->
     <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>)).

============================
 forall G A C D1 D2,
   (nabla x, ctx G -> <A:form> -> <G |- D1:conc A> ->
      <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))

cut_admit < induction on 2.

IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
============================
 forall G A C D1 D2,
   (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
      <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))

cut_admit < induction on 4.

IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
============================
 forall G A C D1 D2,
   (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
      <G, x:hyp A |- D2 x:conc C>@@ -> (exists D3, <G |- D3:conc C>))

cut_admit < intros.

Variables: G A C D1 D2
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- D2 n1:conc C>@@
============================
 exists D3, <G |- D3:conc C>

cut_admit < case H4 (keep).
Subgoal 1:

Variables: G A D1 C1 lf_1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- init C1 (lf_1 n1):conc (atom C1)>@@
H5 : <G, n1:hyp A |- C1:i>**
H6 : <G, n1:hyp A |- lf_1 n1:hyp (atom C1)>**
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H6.
Subgoal 1:

Variables: G A D1 C1 lf_1 F
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- init C1 (lf_1 n1):conc (atom C1)>@@
H5 : <G, n1:hyp A |- C1:i>**
H7 : <G, n1:hyp A, [F n1] |- lf_1 n1:hyp (atom C1)>**
H8 : member (F n1) (<n1:hyp A> :: G)
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H8.
Subgoal 1.1:

Variables: G A D1 C1 lf_1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- init C1 (lf_1 n1):conc (atom C1)>@@
H5 : <G, n1:hyp A |- C1:i>**
H7 : <G, n1:hyp A, [n1:hyp A] |- lf_1 n1:hyp (atom C1)>**
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 1.2 is:
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H7.
Subgoal 1.1:

Variables: G D1 C1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <atom C1:form>@
H3 : <G |- D1:conc (atom C1)>
H4 : <G, n1:hyp (atom C1) |- init C1 n1:conc (atom C1)>@@
H5 : <G, n1:hyp (atom C1) |- C1:i>**
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 1.2 is:
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < search.
Subgoal 1.2:

Variables: G A D1 C1 lf_1 F
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- init C1 (lf_1 n1):conc (atom C1)>@@
H5 : <G, n1:hyp A |- C1:i>**
H7 : <G, n1:hyp A, [F n1] |- lf_1 n1:hyp (atom C1)>**
H9 : member (F n1) G
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply prune to H9.
Subgoal 1.2:

Variables: G A D1 C1 lf_1 F1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- init C1 (lf_1 n1):conc (atom C1)>@@
H5 : <G, n1:hyp A |- C1:i>**
H7 : <G, n1:hyp A, [F1] |- lf_1 n1:hyp (atom C1)>**
H9 : member F1 G
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply ctx_mem to H1 H9.
Subgoal 1.2:

Variables: G A D1 C1 lf_1 A1 P
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- init C1 (lf_1 n1):conc (atom C1)>@@
H5 : <G, n1:hyp A |- C1:i>**
H7 : <G, n1:hyp A, [P:hyp A1] |- lf_1 n1:hyp (atom C1)>**
H9 : member <P:hyp A1> G
H10 : fresh P A1
============================
 exists D3, <G |- D3:conc (atom C1)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H10.
Subgoal 1.2:

Variables: G A D1 C1 lf_1 A2
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx (G n2)
H2 : <A n2:form>@
H3 : <G n2 |- D1 n2:conc (A n2)>
H4 : <G n2, n1:hyp (A n2) |- init (C1 n2) (lf_1 n2 n1):conc (atom (C1 n2))>@@
H5 : <G n2, n1:hyp (A n2) |- C1 n2:i>**
H7 : <G n2, n1:hyp (A n2), [n2:hyp A2] |- lf_1 n2 n1:hyp (atom (C1 n2))>**
H9 : member <n2:hyp A2> (G n2)
============================
 exists D3, <G n2 |- D3:conc (atom (C1 n2))>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H7.
Subgoal 1.2:

Variables: G A D1 A3
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx (G n2)
H2 : <A n2:form>@
H3 : <G n2 |- D1 n2:conc (A n2)>
H4 : <G n2, n1:hyp (A n2) |- init A3 n2:conc (atom A3)>@@
H5 : <G n2, n1:hyp (A n2) |- A3:i>**
H9 : member <n2:hyp (atom A3)> (G n2)
============================
 exists D3, <G n2 |- D3:conc (atom A3)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply strength_i to _ H5.
Subgoal 1.2:

Variables: G A D1 A3
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx (G n2)
H2 : <A n2:form>@
H3 : <G n2 |- D1 n2:conc (A n2)>
H4 : <G n2, n1:hyp (A n2) |- init A3 n2:conc (atom A3)>@@
H5 : <G n2, n1:hyp (A n2) |- A3:i>**
H9 : member <n2:hyp (atom A3)> (G n2)
H11 : <A3:i>
============================
 exists D3, <G n2 |- D3:conc (atom A3)>

Subgoal 2 is:
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < search.
Subgoal 2:

Variables: G A D1 C2 lf_1 C1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impR C1 C2 (lf_1 n1):conc (imp C1 C2)>@@
H5 : <G, n1:hyp A |- C1:form>**
H6 : <G, n1:hyp A |- C2:form>**
H7 : <G, n1:hyp A, n2:hyp C1 |- lf_1 n1 n2:conc C2>**
============================
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply strength_form to _ H5.
Subgoal 2:

Variables: G A D1 C2 lf_1 C1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impR C1 C2 (lf_1 n1):conc (imp C1 C2)>@@
H5 : <G, n1:hyp A |- C1:form>**
H6 : <G, n1:hyp A |- C2:form>**
H7 : <G, n1:hyp A, n2:hyp C1 |- lf_1 n1 n2:conc C2>**
H8 : <C1:form>
============================
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply strength_form to _ H6.
Subgoal 2:

Variables: G A D1 C2 lf_1 C1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impR C1 C2 (lf_1 n1):conc (imp C1 C2)>@@
H5 : <G, n1:hyp A |- C1:form>**
H6 : <G, n1:hyp A |- C2:form>**
H7 : <G, n1:hyp A, n2:hyp C1 |- lf_1 n1 n2:conc C2>**
H8 : <C1:form>
H9 : <C2:form>
============================
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply IH1 to _ H2 H3 H7.
Subgoal 2:

Variables: G A D1 C2 lf_1 C1 D3
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impR C1 C2 (lf_1 n1):conc (imp C1 C2)>@@
H5 : <G, n1:hyp A |- C1:form>**
H6 : <G, n1:hyp A |- C2:form>**
H7 : <G, n1:hyp A, n2:hyp C1 |- lf_1 n1 n2:conc C2>**
H8 : <C1:form>
H9 : <C2:form>
H10 : <G, n2:hyp C1 |- D3 n2:conc C2>
============================
 exists D3, <G |- D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < exists impR C1 C2 D3.
Subgoal 2:

Variables: G A D1 C2 lf_1 C1 D3
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impR C1 C2 (lf_1 n1):conc (imp C1 C2)>@@
H5 : <G, n1:hyp A |- C1:form>**
H6 : <G, n1:hyp A |- C2:form>**
H7 : <G, n1:hyp A, n2:hyp C1 |- lf_1 n1 n2:conc C2>**
H8 : <C1:form>
H9 : <C2:form>
H10 : <G, n2:hyp C1 |- D3 n2:conc C2>
============================
 <G |- impR C1 C2 D3:conc (imp C1 C2)>

Subgoal 3 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < search.
Subgoal 3:

Variables: G A C D1 B A1 lf_3 lf_2 lf_1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL (A1 n1) (B n1) C (lf_1 n1) (lf_2 n1) (lf_3 n1):
        conc C>@@
H5 : <G, n1:hyp A |- A1 n1:form>**
H6 : <G, n1:hyp A |- B n1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc (A1 n1)>**
H9 : <G, n1:hyp A, n2:hyp (B n1) |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp (A1 n1) (B n1))>**
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply strength_form to _ H5.
Subgoal 3:

Variables: G A C D1 B A1 lf_3 lf_2 lf_1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL (A1 n1) (B n1) C (lf_1 n1) (lf_2 n1) (lf_3 n1):
        conc C>@@
H5 : <G, n1:hyp A |- A1 n1:form>**
H6 : <G, n1:hyp A |- B n1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc (A1 n1)>**
H9 : <G, n1:hyp A, n2:hyp (B n1) |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp (A1 n1) (B n1))>**
H11 : <A1 n1:form>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply prune_form to H11.
Subgoal 3:

Variables: G A C D1 B lf_3 lf_2 lf_1 FF
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF (B n1) C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- B n1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp (B n1) |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp FF (B n1))>**
H11 : <FF:form>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply IH1 to H1 H2 H3 H8.
Subgoal 3:

Variables: G A C D1 B lf_3 lf_2 lf_1 FF D3
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF (B n1) C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- B n1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp (B n1) |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp FF (B n1))>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply strength_form to _ H6.
Subgoal 3:

Variables: G A C D1 B lf_3 lf_2 lf_1 FF D3
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF (B n1) C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- B n1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp (B n1) |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp FF (B n1))>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <B n1:form>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply prune_form to H13.
Subgoal 3:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp FF FF1)>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply IH1 to _ H2 H3 H9.
Subgoal 3:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1 D4
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H10 : <G, n1:hyp A |- lf_3 n1:hyp (imp FF FF1)>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H10.
Subgoal 3:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1 D4 F
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H15 : <G, n1:hyp A, [F n1] |- lf_3 n1:hyp (imp FF FF1)>**
H16 : member (F n1) (<n1:hyp A> :: G)
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H16.
Subgoal 3.1:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1 D4
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H15 : <G, n1:hyp A, [n1:hyp A] |- lf_3 n1:hyp (imp FF FF1)>**
============================
 exists D3, <G |- D3:conc C>

Subgoal 3.2 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H15.
Subgoal 3.1:

Variables: G C D1 lf_2 lf_1 FF D3 FF1 D4
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <imp FF FF1:form>@
H3 : <G |- D1:conc (imp FF FF1)>
H4 : <G, n1:hyp (imp FF FF1) |- impL FF FF1 C (lf_1 n1) (lf_2 n1) n1:conc C>@@
H5 : <G, n1:hyp (imp FF FF1) |- FF:form>**
H6 : <G, n1:hyp (imp FF FF1) |- FF1:form>**
H7 : <G, n1:hyp (imp FF FF1) |- C:form>**
H8 : <G, n1:hyp (imp FF FF1) |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp (imp FF FF1), n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
============================
 exists D3, <G |- D3:conc C>

Subgoal 3.2 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply imp_invert to H1 H3.
Subgoal 3.1:

Variables: G C D1 lf_2 lf_1 FF D3 FF1 D4 EE
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <imp FF FF1:form>@
H3 : <G |- D1:conc (imp FF FF1)>
H4 : <G, n1:hyp (imp FF FF1) |- impL FF FF1 C (lf_1 n1) (lf_2 n1) n1:conc C>@@
H5 : <G, n1:hyp (imp FF FF1) |- FF:form>**
H6 : <G, n1:hyp (imp FF FF1) |- FF1:form>**
H7 : <G, n1:hyp (imp FF FF1) |- C:form>**
H8 : <G, n1:hyp (imp FF FF1) |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp (imp FF FF1), n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : <G, n1:hyp FF |- EE n1:conc FF1>
============================
 exists D3, <G |- D3:conc C>

Subgoal 3.2 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H2.
Subgoal 3.1:

Variables: G C D1 lf_2 lf_1 FF D3 FF1 D4 EE
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H3 : <G |- D1:conc (imp FF FF1)>
H4 : <G, n1:hyp (imp FF FF1) |- impL FF FF1 C (lf_1 n1) (lf_2 n1) n1:conc C>@@
H5 : <G, n1:hyp (imp FF FF1) |- FF:form>**
H6 : <G, n1:hyp (imp FF FF1) |- FF1:form>**
H7 : <G, n1:hyp (imp FF FF1) |- C:form>**
H8 : <G, n1:hyp (imp FF FF1) |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp (imp FF FF1), n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : <G, n1:hyp FF |- EE n1:conc FF1>
H18 : <FF:form>*
H19 : <FF1:form>*
============================
 exists D3, <G |- D3:conc C>

Subgoal 3.2 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply IH to H1 H18 H12 H17.
Subgoal 3.1:

Variables: G C D1 lf_2 lf_1 FF D3 FF1 D4 EE D5
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H3 : <G |- D1:conc (imp FF FF1)>
H4 : <G, n1:hyp (imp FF FF1) |- impL FF FF1 C (lf_1 n1) (lf_2 n1) n1:conc C>@@
H5 : <G, n1:hyp (imp FF FF1) |- FF:form>**
H6 : <G, n1:hyp (imp FF FF1) |- FF1:form>**
H7 : <G, n1:hyp (imp FF FF1) |- C:form>**
H8 : <G, n1:hyp (imp FF FF1) |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp (imp FF FF1), n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : <G, n1:hyp FF |- EE n1:conc FF1>
H18 : <FF:form>*
H19 : <FF1:form>*
H20 : <G |- D5:conc FF1>
============================
 exists D3, <G |- D3:conc C>

Subgoal 3.2 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply IH to H1 H19 H20 H14.
Subgoal 3.1:

Variables: G C D1 lf_2 lf_1 FF D3 FF1 D4 EE D5 D6
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H3 : <G |- D1:conc (imp FF FF1)>
H4 : <G, n1:hyp (imp FF FF1) |- impL FF FF1 C (lf_1 n1) (lf_2 n1) n1:conc C>@@
H5 : <G, n1:hyp (imp FF FF1) |- FF:form>**
H6 : <G, n1:hyp (imp FF FF1) |- FF1:form>**
H7 : <G, n1:hyp (imp FF FF1) |- C:form>**
H8 : <G, n1:hyp (imp FF FF1) |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp (imp FF FF1), n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : <G, n1:hyp FF |- EE n1:conc FF1>
H18 : <FF:form>*
H19 : <FF1:form>*
H20 : <G |- D5:conc FF1>
H21 : <G |- D6:conc C>
============================
 exists D3, <G |- D3:conc C>

Subgoal 3.2 is:
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < search.
Subgoal 3.2:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1 D4 F
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H15 : <G, n1:hyp A, [F n1] |- lf_3 n1:hyp (imp FF FF1)>**
H17 : member (F n1) G
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply prune to H17.
Subgoal 3.2:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1 D4 F1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H15 : <G, n1:hyp A, [F1] |- lf_3 n1:hyp (imp FF FF1)>**
H17 : member F1 G
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply ctx_mem to H1 H17.
Subgoal 3.2:

Variables: G A C D1 lf_3 lf_2 lf_1 FF D3 FF1 D4 A2 P
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) (lf_3 n1):conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H15 : <G, n1:hyp A, [P:hyp A2] |- lf_3 n1:hyp (imp FF FF1)>**
H17 : member <P:hyp A2> G
H18 : fresh P A2
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H15.
Subgoal 3.2:

Variables: G A C D1 lf_2 lf_1 FF D3 FF1 D4 P
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) P:conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : member <P:hyp (imp FF FF1)> G
H18 : fresh P (imp FF FF1)
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < apply strength_form to _ H7.
Subgoal 3.2:

Variables: G A C D1 lf_2 lf_1 FF D3 FF1 D4 P
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) P:conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : member <P:hyp (imp FF FF1)> G
H18 : fresh P (imp FF FF1)
H19 : <C:form>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < assert <G |- impL FF FF1 C D3 D4 P:conc C>.
Subgoal 3.2:

Variables: G A C D1 lf_2 lf_1 FF D3 FF1 D4 P
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- impL FF FF1 C (lf_1 n1) (lf_2 n1) P:conc C>@@
H5 : <G, n1:hyp A |- FF:form>**
H6 : <G, n1:hyp A |- FF1:form>**
H7 : <G, n1:hyp A |- C:form>**
H8 : <G, n1:hyp A |- lf_1 n1:conc FF>**
H9 : <G, n1:hyp A, n2:hyp FF1 |- lf_2 n1 n2:conc C>**
H11 : <FF:form>
H12 : <G |- D3:conc FF>
H13 : <FF1:form>
H14 : <G, n2:hyp FF1 |- D4 n2:conc C>
H17 : member <P:hyp (imp FF FF1)> G
H18 : fresh P (imp FF FF1)
H19 : <C:form>
H20 : <G |- impL FF FF1 C D3 D4 P:conc C>
============================
 exists D3, <G |- D3:conc C>

Subgoal 4 is:
 exists D3, <G |- D3:conc C>

cut_admit < search.
Subgoal 4:

Variables: G A C D1 D2 F
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- D2 n1:conc C>@@
H5 : <G, n1:hyp A, [F n1] |- D2 n1:conc C>**
H6 : member (F n1) (<n1:hyp A> :: G)
============================
 exists D3, <G |- D3:conc C>

cut_admit < case H6.
Subgoal 4.1:

Variables: G A C D1 D2
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- D2 n1:conc C>@@
H5 : <G, n1:hyp A, [n1:hyp A] |- D2 n1:conc C>**
============================
 exists D3, <G |- D3:conc C>

Subgoal 4.2 is:
 exists D3, <G |- D3:conc C>

cut_admit < case H5.
Subgoal 4.2:

Variables: G A C D1 D2 F
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- D2 n1:conc C>@@
H5 : <G, n1:hyp A, [F n1] |- D2 n1:conc C>**
H7 : member (F n1) G
============================
 exists D3, <G |- D3:conc C>

cut_admit < apply prune to H7.
Subgoal 4.2:

Variables: G A C D1 D2 F1
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- D2 n1:conc C>@@
H5 : <G, n1:hyp A, [F1] |- D2 n1:conc C>**
H7 : member F1 G
============================
 exists D3, <G |- D3:conc C>

cut_admit < apply ctx_mem to H1 H7.
Subgoal 4.2:

Variables: G A C D1 D2 A1 P
IH : forall G A C D1 D2,
       (nabla x, ctx G -> <A:form>* -> <G |- D1:conc A> ->
          <G, x:hyp A |- D2 x:conc C> -> (exists D3, <G |- D3:conc C>))
IH1 : forall G A C D1 D2,
        (nabla x, ctx G -> <A:form>@ -> <G |- D1:conc A> ->
           <G, x:hyp A |- D2 x:conc C>** -> (exists D3, <G |- D3:conc C>))
H1 : ctx G
H2 : <A:form>@
H3 : <G |- D1:conc A>
H4 : <G, n1:hyp A |- D2 n1:conc C>@@
H5 : <G, n1:hyp A, [P:hyp A1] |- D2 n1:conc C>**
H7 : member <P:hyp A1> G
H8 : fresh P A1
============================
 exists D3, <G |- D3:conc C>

cut_admit < case H5.
Proof completed.
Abella < Goodbye.