Welcome to Abella 2.0.5-dev.
Abella < Specification "equiv".
Reading specification "equiv".

Abella < Define ctxs : olist -> olist -> olist -> prop by 
ctxs nil nil nil;
ctxs (nd G :: L) (hyp G :: J) (hil G :: K) := ctxs L J K.

Abella < Theorem ctxs_member1 : 
forall L J K E, ctxs L J K -> member E L ->
  (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K).


============================
 forall L J K E, ctxs L J K -> member E L ->
   (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)

ctxs_member1 < induction on 2.

IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
============================
 forall L J K E, ctxs L J K -> member E L @ ->
   (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)

ctxs_member1 < intros.

Variables: L J K E
IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
H1 : ctxs L J K
H2 : member E L @
============================
 exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K

ctxs_member1 < case H2.
Subgoal 1:

Variables: J K E L1
IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
H1 : ctxs (E :: L1) J K
============================
 exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K

Subgoal 2 is:
 exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K

ctxs_member1 < case H1.
Subgoal 1:

Variables: L1 K1 G J1
IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
H3 : ctxs L1 J1 K1
============================
 exists F, nd G = nd F /\ member (hyp F) (hyp G :: J1) /\
   member (hil F) (hil G :: K1)

Subgoal 2 is:
 exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K

ctxs_member1 < search.
Subgoal 2:

Variables: J K E L1 B
IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
H1 : ctxs (B :: L1) J K
H3 : member E L1 *
============================
 exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K

ctxs_member1 < case H1.
Subgoal 2:

Variables: E L1 K1 G J1
IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
H3 : member E L1 *
H4 : ctxs L1 J1 K1
============================
 exists F, E = nd F /\ member (hyp F) (hyp G :: J1) /\
   member (hil F) (hil G :: K1)

ctxs_member1 < apply IH to H4 H3.
Subgoal 2:

Variables: L1 K1 G J1 F
IH : forall L J K E, ctxs L J K -> member E L * ->
       (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K)
H3 : member (nd F) L1 *
H4 : ctxs L1 J1 K1
H5 : member (hyp F) J1
H6 : member (hil F) K1
============================
 exists F1, nd F = nd F1 /\ member (hyp F1) (hyp G :: J1) /\
   member (hil F1) (hil G :: K1)

ctxs_member1 < search.
Proof completed.
Abella < Theorem ctxs_member2 : 
forall L J K E, ctxs L J K -> member E J ->
  (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K).


============================
 forall L J K E, ctxs L J K -> member E J ->
   (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)

ctxs_member2 < induction on 2.

IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
============================
 forall L J K E, ctxs L J K -> member E J @ ->
   (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)

ctxs_member2 < intros.

Variables: L J K E
IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
H1 : ctxs L J K
H2 : member E J @
============================
 exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K

ctxs_member2 < case H2.
Subgoal 1:

Variables: L K E L1
IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
H1 : ctxs L (E :: L1) K
============================
 exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K

Subgoal 2 is:
 exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K

ctxs_member2 < case H1.
Subgoal 1:

Variables: L1 K1 G L2
IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
H3 : ctxs L2 L1 K1
============================
 exists F, hyp G = hyp F /\ member (nd F) (nd G :: L2) /\
   member (hil F) (hil G :: K1)

Subgoal 2 is:
 exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K

ctxs_member2 < search.
Subgoal 2:

Variables: L K E L1 B
IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
H1 : ctxs L (B :: L1) K
H3 : member E L1 *
============================
 exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K

ctxs_member2 < case H1.
Subgoal 2:

Variables: E L1 K1 G L2
IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
H3 : member E L1 *
H4 : ctxs L2 L1 K1
============================
 exists F, E = hyp F /\ member (nd F) (nd G :: L2) /\
   member (hil F) (hil G :: K1)

ctxs_member2 < apply IH to H4 H3.
Subgoal 2:

Variables: L1 K1 G L2 F
IH : forall L J K E, ctxs L J K -> member E J * ->
       (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K)
H3 : member (hyp F) L1 *
H4 : ctxs L2 L1 K1
H5 : member (nd F) L2
H6 : member (hil F) K1
============================
 exists F1, hyp F = hyp F1 /\ member (nd F1) (nd G :: L2) /\
   member (hil F1) (hil G :: K1)

ctxs_member2 < search.
Proof completed.
Abella < Theorem ctxs_member3 : 
forall L J K E, ctxs L J K -> member E K ->
  (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J).


============================
 forall L J K E, ctxs L J K -> member E K ->
   (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)

ctxs_member3 < induction on 2.

IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
============================
 forall L J K E, ctxs L J K -> member E K @ ->
   (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)

ctxs_member3 < intros.

Variables: L J K E
IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
H1 : ctxs L J K
H2 : member E K @
============================
 exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J

ctxs_member3 < case H2.
Subgoal 1:

Variables: L J E L1
IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
H1 : ctxs L J (E :: L1)
============================
 exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J

Subgoal 2 is:
 exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J

ctxs_member3 < case H1.
Subgoal 1:

Variables: L1 G J1 L2
IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
H3 : ctxs L2 J1 L1
============================
 exists F, hil G = hil F /\ member (nd F) (nd G :: L2) /\
   member (hyp F) (hyp G :: J1)

Subgoal 2 is:
 exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J

ctxs_member3 < search.
Subgoal 2:

Variables: L J E L1 B
IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
H1 : ctxs L J (B :: L1)
H3 : member E L1 *
============================
 exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J

ctxs_member3 < case H1.
Subgoal 2:

Variables: E L1 G J1 L2
IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
H3 : member E L1 *
H4 : ctxs L2 J1 L1
============================
 exists F, E = hil F /\ member (nd F) (nd G :: L2) /\
   member (hyp F) (hyp G :: J1)

ctxs_member3 < apply IH to H4 H3.
Subgoal 2:

Variables: L1 G J1 L2 F
IH : forall L J K E, ctxs L J K -> member E K * ->
       (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J)
H3 : member (hil F) L1 *
H4 : ctxs L2 J1 L1
H5 : member (nd F) L2
H6 : member (hyp F) J1
============================
 exists F1, hil F = hil F1 /\ member (nd F1) (nd G :: L2) /\
   member (hyp F1) (hyp G :: J1)

ctxs_member3 < search.
Proof completed.
Abella < Theorem nd_to_seq_ext : 
forall L J K G, ctxs L J K -> {L |- nd G} -> {J |- conc G}.


============================
 forall L J K G, ctxs L J K -> {L |- nd G} -> {J |- conc G}

nd_to_seq_ext < induction on 2.

IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
============================
 forall L J K G, ctxs L J K -> {L |- nd G}@ -> {J |- conc G}

nd_to_seq_ext < intros.

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H2 : {L |- nd G}@
============================
 {J |- conc G}

nd_to_seq_ext < case H2.
Subgoal 1:

Variables: L J K B A
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L, nd A |- nd B}*
============================
 {J |- conc (imp A B)}

Subgoal 2 is:
 {J |- conc G}

Subgoal 3 is:
 {J |- conc G}

nd_to_seq_ext < apply IH to _ H3.
Subgoal 1:

Variables: L J K B A
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L, nd A |- nd B}*
H4 : {J, hyp A |- conc B}
============================
 {J |- conc (imp A B)}

Subgoal 2 is:
 {J |- conc G}

Subgoal 3 is:
 {J |- conc G}

nd_to_seq_ext < search.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L |- nd (imp A G)}*
H4 : {L |- nd A}*
============================
 {J |- conc G}

Subgoal 3 is:
 {J |- conc G}

nd_to_seq_ext < apply IH to H1 H3.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L |- nd (imp A G)}*
H4 : {L |- nd A}*
H5 : {J |- conc (imp A G)}
============================
 {J |- conc G}

Subgoal 3 is:
 {J |- conc G}

nd_to_seq_ext < apply IH to H1 H4.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L |- nd (imp A G)}*
H4 : {L |- nd A}*
H5 : {J |- conc (imp A G)}
H6 : {J |- conc A}
============================
 {J |- conc G}

Subgoal 3 is:
 {J |- conc G}

nd_to_seq_ext < search.
Subgoal 3:

Variables: L J K G F
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L, [F] |- nd G}*
H4 : member F L
============================
 {J |- conc G}

nd_to_seq_ext < apply ctxs_member1 to H1 H4.
Subgoal 3:

Variables: L J K G F1
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H3 : {L, [nd F1] |- nd G}*
H4 : member (nd F1) L
H5 : member (hyp F1) J
H6 : member (hil F1) K
============================
 {J |- conc G}

nd_to_seq_ext < case H3.
Subgoal 3:

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G}
H1 : ctxs L J K
H4 : member (nd G) L
H5 : member (hyp G) J
H6 : member (hil G) K
============================
 {J |- conc G}

nd_to_seq_ext < search.
Proof completed.
Abella < Theorem nd_to_seq : 
forall G, {nd G} -> {conc G}.


============================
 forall G, {nd G} -> {conc G}

nd_to_seq < intros.

Variables: G
H1 : {nd G}
============================
 {conc G}

nd_to_seq < apply nd_to_seq_ext to _ H1.

Variables: G
H1 : {nd G}
H2 : {conc G}
============================
 {conc G}

nd_to_seq < search.
Proof completed.
Abella < Set witnesses on.

Abella < Theorem hil_deduction : 
forall L J K A B, ctxs L J K -> {K, hil A |- hil B} -> {K |- hil (imp A B)}.


============================
 forall L J K A B, ctxs L J K -> {K, hil A |- hil B} -> {K |- hil (imp A B)}

hil_deduction < induction on 2.

IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
============================
 forall L J K A B, ctxs L J K -> {K, hil A |- hil B}@ -> {K |- hil (imp A B)}

hil_deduction < intros.

Variables: L J K A B
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H2 : {K, hil A |- hil B}@
============================
 {K |- hil (imp A B)}

hil_deduction < case H2.
Subgoal 1:

Variables: L J K A A1 B1
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
============================
 {K |- hil (imp A (imp A1 (imp B1 A1)))}

Subgoal 2 is:
 {K |- hil (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil (imp A B)}

hil_deduction < search.
Witness: unfold(hil, 3, unfold(hil, 1), unfold(hil, 1)).
Subgoal 2:

Variables: L J K A C A1 B1
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
============================
 {K |- hil (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil (imp A B)}

hil_deduction < search.
Witness: unfold(hil, 3, unfold(hil, 1), unfold(hil, 2)).
Subgoal 3:

Variables: L J K A B A1
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A |- hil (imp A1 B)}*
H4 : {K, hil A |- hil A1}*
============================
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil (imp A B)}

hil_deduction < apply IH to _ H3.
Witness: apply H1.
Subgoal 3:

Variables: L J K A B A1
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A |- hil (imp A1 B)}*
H4 : {K, hil A |- hil A1}*
H5 : {K |- hil (imp A (imp A1 B))}
============================
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil (imp A B)}

hil_deduction < apply IH to _ H4.
Witness: apply H1.
Subgoal 3:

Variables: L J K A B A1
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A |- hil (imp A1 B)}*
H4 : {K, hil A |- hil A1}*
H5 : {K |- hil (imp A (imp A1 B))}
H6 : {K |- hil (imp A A1)}
============================
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil (imp A B)}

hil_deduction < search.
Witness: unfold(hil, 3, unfold(hil, 3, unfold(hil, 1), unfold(hil, 3, unfold(hil, 3, unfold(hil, 2), apply H5), apply H6)), apply H5).
Subgoal 4:

Variables: L J K A B F
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A, [F] |- hil B}*
H4 : member F (hil A :: K)
============================
 {K |- hil (imp A B)}

hil_deduction < case H4.
Subgoal 4.1:

Variables: L J K A B
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A, [hil A] |- hil B}*
============================
 {K |- hil (imp A B)}

Subgoal 4.2 is:
 {K |- hil (imp A B)}

hil_deduction < case H3.
Subgoal 4.1:

Variables: L J K B
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
============================
 {K |- hil (imp B B)}

Subgoal 4.2 is:
 {K |- hil (imp A B)}

hil_deduction < search.
Witness: unfold(hil, 3, unfold(hil, 3, unfold(hil, 1), unfold(hil, 3, unfold(hil, 3, unfold(hil, 2), unfold(hil, 1)), unfold(hil, 1))), unfold(hil, 1)).
Subgoal 4.2:

Variables: L J K A B F
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A, [F] |- hil B}*
H5 : member F K
============================
 {K |- hil (imp A B)}

hil_deduction < apply ctxs_member3 to H1 H5.
Subgoal 4.2:

Variables: L J K A B F1
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H3 : {K, hil A, [hil F1] |- hil B}*
H5 : member (hil F1) K
H6 : member (nd F1) L
H7 : member (hyp F1) J
============================
 {K |- hil (imp A B)}

hil_deduction < case H3.
Subgoal 4.2:

Variables: L J K A B
IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* ->
       {K |- hil (imp A B)}
H1 : ctxs L J K
H5 : member (hil B) K
H6 : member (nd B) L
H7 : member (hyp B) J
============================
 {K |- hil (imp A B)}

hil_deduction < search.
Witness: unfold(hil, 3, unfold(hil, 1), unfold(hil, 3, unfold(hil, 3, unfold(hil, 1), unfold(hil, 1)), unfold(hil, 1))).
Proof completed.
Abella < Set witnesses off.

Abella < Theorem seq_to_hil_ext : 
forall L J K G, ctxs L J K -> {J |- conc G} -> {K |- hil G}.


============================
 forall L J K G, ctxs L J K -> {J |- conc G} -> {K |- hil G}

seq_to_hil_ext < induction on 2.

IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
============================
 forall L J K G, ctxs L J K -> {J |- conc G}@ -> {K |- hil G}

seq_to_hil_ext < intros.

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H2 : {J |- conc G}@
============================
 {K |- hil G}

seq_to_hil_ext < case H2.
Subgoal 1:

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J |- hyp G}*
============================
 {K |- hil G}

Subgoal 2 is:
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < case H3.
Subgoal 1:

Variables: L J K G F
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J, [F] |- hyp G}*
H5 : member F J
============================
 {K |- hil G}

Subgoal 2 is:
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply ctxs_member2 to H1 H5.
Subgoal 1:

Variables: L J K G F1
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J, [hyp F1] |- hyp G}*
H5 : member (hyp F1) J
H6 : member (nd F1) L
H7 : member (hil F1) K
============================
 {K |- hil G}

Subgoal 2 is:
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < case H4.
Subgoal 1:

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H5 : member (hyp G) J
H6 : member (nd G) L
H7 : member (hil G) K
============================
 {K |- hil G}

Subgoal 2 is:
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < search.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc G}*
H4 : {J |- conc A}*
============================
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply IH to _ H3.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc G}*
H4 : {J |- conc A}*
H5 : {K, hil A |- hil G}
============================
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply IH to H1 H4.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc G}*
H4 : {J |- conc A}*
H5 : {K, hil A |- hil G}
H6 : {K |- hil A}
============================
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply hil_deduction to _ H5.
Subgoal 2:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc G}*
H4 : {J |- conc A}*
H5 : {K, hil A |- hil G}
H6 : {K |- hil A}
H7 : {K |- hil (imp A G)}
============================
 {K |- hil G}

Subgoal 3 is:
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < search.
Subgoal 3:

Variables: L J K B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc B}*
============================
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply IH to _ H3.
Subgoal 3:

Variables: L J K B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc B}*
H4 : {K, hil A |- hil B}
============================
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply hil_deduction to _ H4.
Subgoal 3:

Variables: L J K B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, hyp A |- conc B}*
H4 : {K, hil A |- hil B}
H5 : {K |- hil (imp A B)}
============================
 {K |- hil (imp A B)}

Subgoal 4 is:
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < search.
Subgoal 4:

Variables: L J K G B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J |- hyp (imp A B)}*
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < case H3.
Subgoal 4:

Variables: L J K G B A F
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
H6 : {J, [F] |- hyp (imp A B)}*
H7 : member F J
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply ctxs_member2 to H1 H7.
Subgoal 4:

Variables: L J K G B A F1
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
H6 : {J, [hyp F1] |- hyp (imp A B)}*
H7 : member (hyp F1) J
H8 : member (nd F1) L
H9 : member (hil F1) K
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < case H6.
Subgoal 4:

Variables: L J K G B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
H7 : member (hyp (imp A B)) J
H8 : member (nd (imp A B)) L
H9 : member (hil (imp A B)) K
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply IH to H1 H4.
Subgoal 4:

Variables: L J K G B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
H7 : member (hyp (imp A B)) J
H8 : member (nd (imp A B)) L
H9 : member (hil (imp A B)) K
H10 : {K |- hil A}
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply IH to _ H5.
Subgoal 4:

Variables: L J K G B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
H7 : member (hyp (imp A B)) J
H8 : member (nd (imp A B)) L
H9 : member (hil (imp A B)) K
H10 : {K |- hil A}
H11 : {K, hil B |- hil G}
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < apply hil_deduction to _ H11.
Subgoal 4:

Variables: L J K G B A
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H4 : {J |- conc A}*
H5 : {J, hyp B |- conc G}*
H7 : member (hyp (imp A B)) J
H8 : member (nd (imp A B)) L
H9 : member (hil (imp A B)) K
H10 : {K |- hil A}
H11 : {K, hil B |- hil G}
H12 : {K |- hil (imp B G)}
============================
 {K |- hil G}

Subgoal 5 is:
 {K |- hil G}

seq_to_hil_ext < search.
Subgoal 5:

Variables: L J K G F
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, [F] |- conc G}*
H4 : member F J
============================
 {K |- hil G}

seq_to_hil_ext < apply ctxs_member2 to H1 H4.
Subgoal 5:

Variables: L J K G F1
IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G}
H1 : ctxs L J K
H3 : {J, [hyp F1] |- conc G}*
H4 : member (hyp F1) J
H5 : member (nd F1) L
H6 : member (hil F1) K
============================
 {K |- hil G}

seq_to_hil_ext < case H3.
Proof completed.
Abella < Theorem seq_to_hil : 
forall G, {conc G} -> {hil G}.


============================
 forall G, {conc G} -> {hil G}

seq_to_hil < intros.

Variables: G
H1 : {conc G}
============================
 {hil G}

seq_to_hil < apply seq_to_hil_ext to _ H1.

Variables: G
H1 : {conc G}
H2 : {hil G}
============================
 {hil G}

seq_to_hil < search.
Proof completed.
Abella < Theorem hil_to_nd_ext : 
forall L J K G, ctxs L J K -> {K |- hil G} -> {L |- nd G}.


============================
 forall L J K G, ctxs L J K -> {K |- hil G} -> {L |- nd G}

hil_to_nd_ext < induction on 2.

IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
============================
 forall L J K G, ctxs L J K -> {K |- hil G}@ -> {L |- nd G}

hil_to_nd_ext < intros.

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H2 : {K |- hil G}@
============================
 {L |- nd G}

hil_to_nd_ext < case H2.
Subgoal 1:

Variables: L J K A B
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
============================
 {L |- nd (imp A (imp B A))}

Subgoal 2 is:
 {L |- nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))}

Subgoal 3 is:
 {L |- nd G}

Subgoal 4 is:
 {L |- nd G}

hil_to_nd_ext < search.
Subgoal 2:

Variables: L J K C A B
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
============================
 {L |- nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))}

Subgoal 3 is:
 {L |- nd G}

Subgoal 4 is:
 {L |- nd G}

hil_to_nd_ext < assert {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C}.
Subgoal 2:

Variables: L J K C A B
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H3 : {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C}
============================
 {L |- nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))}

Subgoal 3 is:
 {L |- nd G}

Subgoal 4 is:
 {L |- nd G}

hil_to_nd_ext < search.
Subgoal 3:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H3 : {K |- hil (imp A G)}*
H4 : {K |- hil A}*
============================
 {L |- nd G}

Subgoal 4 is:
 {L |- nd G}

hil_to_nd_ext < apply IH to H1 H3.
Subgoal 3:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H3 : {K |- hil (imp A G)}*
H4 : {K |- hil A}*
H5 : {L |- nd (imp A G)}
============================
 {L |- nd G}

Subgoal 4 is:
 {L |- nd G}

hil_to_nd_ext < apply IH to H1 H4.
Subgoal 3:

Variables: L J K G A
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H3 : {K |- hil (imp A G)}*
H4 : {K |- hil A}*
H5 : {L |- nd (imp A G)}
H6 : {L |- nd A}
============================
 {L |- nd G}

Subgoal 4 is:
 {L |- nd G}

hil_to_nd_ext < search.
Subgoal 4:

Variables: L J K G F
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H3 : {K, [F] |- hil G}*
H4 : member F K
============================
 {L |- nd G}

hil_to_nd_ext < apply ctxs_member3 to H1 H4.
Subgoal 4:

Variables: L J K G F1
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H3 : {K, [hil F1] |- hil G}*
H4 : member (hil F1) K
H5 : member (nd F1) L
H6 : member (hyp F1) J
============================
 {L |- nd G}

hil_to_nd_ext < case H3.
Subgoal 4:

Variables: L J K G
IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G}
H1 : ctxs L J K
H4 : member (hil G) K
H5 : member (nd G) L
H6 : member (hyp G) J
============================
 {L |- nd G}

hil_to_nd_ext < search.
Proof completed.
Abella < Theorem hil_to_nd : 
forall G, {hil G} -> {nd G}.


============================
 forall G, {hil G} -> {nd G}

hil_to_nd < intros.

Variables: G
H1 : {hil G}
============================
 {nd G}

hil_to_nd < apply hil_to_nd_ext to _ H1.

Variables: G
H1 : {hil G}
H2 : {nd G}
============================
 {nd G}

hil_to_nd < search.
Proof completed.
Abella < Define fold : olist -> form -> form -> prop by 
fold nil B B;
fold (hil A :: L) B B' := fold L (imp A B) B'.

Abella < Theorem hil_deduction_generalized : 
forall L J K B B', ctxs L J K -> fold K B B' -> {K |- hil B} -> {hil B'}.


============================
 forall L J K B B', ctxs L J K -> fold K B B' -> {K |- hil B} -> {hil B'}

hil_deduction_generalized < induction on 2.

IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
============================
 forall L J K B B', ctxs L J K -> fold K B B' @ -> {K |- hil B} -> {hil B'}

hil_deduction_generalized < intros.

Variables: L J K B B'
IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
H1 : ctxs L J K
H2 : fold K B B' @
H3 : {K |- hil B}
============================
 {hil B'}

hil_deduction_generalized < case H2.
Subgoal 1:

Variables: L J B'
IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
H1 : ctxs L J nil
H3 : {hil B'}
============================
 {hil B'}

Subgoal 2 is:
 {hil B'}

hil_deduction_generalized < search.
Subgoal 2:

Variables: L J B B' L1 A
IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
H1 : ctxs L J (hil A :: L1)
H3 : {L1, hil A |- hil B}
H4 : fold L1 (imp A B) B' *
============================
 {hil B'}

hil_deduction_generalized < case H1.
Subgoal 2:

Variables: B B' L1 A J1 L2
IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
H3 : {L1, hil A |- hil B}
H4 : fold L1 (imp A B) B' *
H5 : ctxs L2 J1 L1
============================
 {hil B'}

hil_deduction_generalized < apply hil_deduction to _ H3.
Subgoal 2:

Variables: B B' L1 A J1 L2
IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
H3 : {L1, hil A |- hil B}
H4 : fold L1 (imp A B) B' *
H5 : ctxs L2 J1 L1
H6 : {L1 |- hil (imp A B)}
============================
 {hil B'}

hil_deduction_generalized < apply IH to _ H4 H6.
Subgoal 2:

Variables: B B' L1 A J1 L2
IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} ->
       {hil B'}
H3 : {L1, hil A |- hil B}
H4 : fold L1 (imp A B) B' *
H5 : ctxs L2 J1 L1
H6 : {L1 |- hil (imp A B)}
H7 : {hil B'}
============================
 {hil B'}

hil_deduction_generalized < search.
Proof completed.
Abella <