Welcome to Abella 2.0.4-dev
Abella < Specification "poplmark-1a".
Reading specification "poplmark-1a"

Abella < Define name : ty -> prop by 
nabla x, name x.

Abella < Define ctx : olist -> prop by 
ctx nil;
ctx (bound X U :: L) := name X /\ ctx L.

Abella < Define cty : olist -> ty -> prop by 
cty L top;
cty L X := exists U, member (bound X U) L;
cty L (arrow T1 T2) := cty L T1 /\ cty L T2;
cty L (all T1 T2) := cty L T1 /\ (nabla x, cty (bound x T1 :: L) (T2 x)).

Abella < Define ty : ty -> prop by 
ty top;
nabla x, ty x;
ty (arrow T1 T2) := ty T1 /\ ty T2;
ty (all T1 T2) := ty T1 /\ (nabla x, ty (T2 x)).

Abella < Theorem sub_refl : 
forall L T, cty L T -> {L |- sub T T}.


============================
 forall L T, cty L T -> {L |- sub T T}

sub_refl < induction on 1.

IH : forall L T, cty L T * -> {L |- sub T T}
============================
 forall L T, cty L T @ -> {L |- sub T T}

sub_refl < intros.

Variables: L T
IH : forall L T, cty L T * -> {L |- sub T T}
H1 : cty L T @
============================
 {L |- sub T T}

sub_refl < case H1.
Subgoal 1:

Variables: L
IH : forall L T, cty L T * -> {L |- sub T T}
============================
 {L |- sub top top}

Subgoal 2 is:
 {L |- sub T T}

Subgoal 3 is:
 {L |- sub (arrow T1 T2) (arrow T1 T2)}

Subgoal 4 is:
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < search.
Subgoal 2:

Variables: L T U
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : member (bound T U) L
============================
 {L |- sub T T}

Subgoal 3 is:
 {L |- sub (arrow T1 T2) (arrow T1 T2)}

Subgoal 4 is:
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < search.
Subgoal 3:

Variables: L T2 T1
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : cty L T1 *
H3 : cty L T2 *
============================
 {L |- sub (arrow T1 T2) (arrow T1 T2)}

Subgoal 4 is:
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < apply IH to H2.
Subgoal 3:

Variables: L T2 T1
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : cty L T1 *
H3 : cty L T2 *
H4 : {L |- sub T1 T1}
============================
 {L |- sub (arrow T1 T2) (arrow T1 T2)}

Subgoal 4 is:
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < apply IH to H3.
Subgoal 3:

Variables: L T2 T1
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : cty L T1 *
H3 : cty L T2 *
H4 : {L |- sub T1 T1}
H5 : {L |- sub T2 T2}
============================
 {L |- sub (arrow T1 T2) (arrow T1 T2)}

Subgoal 4 is:
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < search.
Subgoal 4:

Variables: L T2 T1
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : cty L T1 *
H3 : cty (bound n1 T1 :: L) (T2 n1) *
============================
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < apply IH to H2.
Subgoal 4:

Variables: L T2 T1
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : cty L T1 *
H3 : cty (bound n1 T1 :: L) (T2 n1) *
H4 : {L |- sub T1 T1}
============================
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < apply IH to H3.
Subgoal 4:

Variables: L T2 T1
IH : forall L T, cty L T * -> {L |- sub T T}
H2 : cty L T1 *
H3 : cty (bound n1 T1 :: L) (T2 n1) *
H4 : {L |- sub T1 T1}
H5 : {L, bound n1 T1 |- sub (T2 n1) (T2 n1)}
============================
 {L |- sub (all T1 T2) (all T1 T2)}

sub_refl < search.
Proof completed.
Abella < Theorem ctx_member : 
forall E L, ctx L -> member E L -> (exists X U, E = bound X U /\ name X).


============================
 forall E L, ctx L -> member E L -> (exists X U, E = bound X U /\ name X)

ctx_member < induction on 2.

IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
============================
 forall E L, ctx L -> member E L @ -> (exists X U, E = bound X U /\ name X)

ctx_member < intros.

Variables: E L
IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
H1 : ctx L
H2 : member E L @
============================
 exists X U, E = bound X U /\ name X

ctx_member < case H2.
Subgoal 1:

Variables: E L1
IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
H1 : ctx (E :: L1)
============================
 exists X U, E = bound X U /\ name X

Subgoal 2 is:
 exists X U, E = bound X U /\ name X

ctx_member < case H1.
Subgoal 1:

Variables: L1 U X
IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
H3 : name X
H4 : ctx L1
============================
 exists X1 U1, bound X U = bound X1 U1 /\ name X1

Subgoal 2 is:
 exists X U, E = bound X U /\ name X

ctx_member < search.
Subgoal 2:

Variables: E L1 B
IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
H1 : ctx (B :: L1)
H3 : member E L1 *
============================
 exists X U, E = bound X U /\ name X

ctx_member < case H1.
Subgoal 2:

Variables: E L1 U X
IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
H3 : member E L1 *
H4 : name X
H5 : ctx L1
============================
 exists X U, E = bound X U /\ name X

ctx_member < apply IH to H5 H3.
Subgoal 2:

Variables: L1 U X X1 U1
IH : forall E L, ctx L -> member E L * ->
       (exists X U, E = bound X U /\ name X)
H3 : member (bound X1 U1) L1 *
H4 : name X
H5 : ctx L1
H6 : name X1
============================
 exists X U, bound X1 U1 = bound X U /\ name X

ctx_member < search.
Proof completed.
Abella < Theorem bound_name : 
forall L X U, ctx L -> {L |- bound X U} -> name X.


============================
 forall L X U, ctx L -> {L |- bound X U} -> name X

bound_name < intros.

Variables: L X U
H1 : ctx L
H2 : {L |- bound X U}
============================
 name X

bound_name < case H2.

Variables: L X U F
H1 : ctx L
H3 : {L, [F] |- bound X U}
H4 : member F L
============================
 name X

bound_name < apply ctx_member to H1 H4.

Variables: L X U X1 U1
H1 : ctx L
H3 : {L, [bound X1 U1] |- bound X U}
H4 : member (bound X1 U1) L
H5 : name X1
============================
 name X

bound_name < case H3.

Variables: L X U
H1 : ctx L
H4 : member (bound X U) L
H5 : name X
============================
 name X

bound_name < search.
Proof completed.
Abella < Theorem sub_top : 
forall L T, ctx L -> {L |- sub top T} -> T = top.


============================
 forall L T, ctx L -> {L |- sub top T} -> T = top

sub_top < intros.

Variables: L T
H1 : ctx L
H2 : {L |- sub top T}
============================
 T = top

sub_top < case H2.
Subgoal 1:

Variables: L
H1 : ctx L
============================
 top = top

Subgoal 2 is:
 top = top

Subgoal 3 is:
 T = top

Subgoal 4 is:
 T = top

sub_top < search.
Subgoal 2:

Variables: L U
H1 : ctx L
H3 : {L |- bound top U}
============================
 top = top

Subgoal 3 is:
 T = top

Subgoal 4 is:
 T = top

sub_top < search.
Subgoal 3:

Variables: L T U
H1 : ctx L
H3 : {L |- bound top U}
H4 : {L |- sub U T}
============================
 T = top

Subgoal 4 is:
 T = top

sub_top < apply bound_name to H1 H3.
Subgoal 3:

Variables: L T U
H1 : ctx L
H3 : {L |- bound top U}
H4 : {L |- sub U T}
H5 : name top
============================
 T = top

Subgoal 4 is:
 T = top

sub_top < case H5.
Subgoal 4:

Variables: L T F
H1 : ctx L
H3 : {L, [F] |- sub top T}
H4 : member F L
============================
 T = top

sub_top < apply ctx_member to H1 H4.
Subgoal 4:

Variables: L T X U
H1 : ctx L
H3 : {L, [bound X U] |- sub top T}
H4 : member (bound X U) L
H5 : name X
============================
 T = top

sub_top < case H3.
Proof completed.
Abella < Theorem dual_theorem : 
forall Q, ty Q ->
  (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} -> {L |- sub S T}) /\
  (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
       {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}).


============================
 forall Q, ty Q ->
   (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
        {L |- sub S T}) /\
   (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})

dual_theorem < induction on 1.

IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
============================
 forall Q, ty Q @ ->
   (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
        {L |- sub S T}) /\
   (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})

dual_theorem < intros.

Variables: Q
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
============================
 (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} -> {L |- sub S T}) /\
   (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})

dual_theorem < split*.
Subgoal 1:

Variables: Q
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
============================
 forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} -> {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < induction on 2.
Subgoal 1:

Variables: Q
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
============================
 forall L S T, ctx L -> {L |- sub S Q}@@ -> {L |- sub Q T} -> {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < intros.
Subgoal 1:

Variables: Q L S T
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
H2 : ctx L
H3 : {L |- sub S Q}@@
H4 : {L |- sub Q T}
============================
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H3.
Subgoal 1.1:

Variables: L S T
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty top @
IH1 : forall L S T, ctx L -> {L |- sub S top}** -> {L |- sub top T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub top T}
============================
 {L |- sub S T}

Subgoal 1.2 is:
 {L |- sub Q T}

Subgoal 1.3 is:
 {L |- sub S T}

Subgoal 1.4 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply sub_top to H2 H4.
Subgoal 1.1:

Variables: L S
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty top @
IH1 : forall L S T, ctx L -> {L |- sub S top}** -> {L |- sub top T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub top top}
============================
 {L |- sub S top}

Subgoal 1.2 is:
 {L |- sub Q T}

Subgoal 1.3 is:
 {L |- sub S T}

Subgoal 1.4 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.2:

Variables: Q L T U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub Q T}
H5 : {L |- bound Q U}**
============================
 {L |- sub Q T}

Subgoal 1.3 is:
 {L |- sub S T}

Subgoal 1.4 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.3:

Variables: Q L S T U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub Q T}
H5 : {L |- bound S U}**
H6 : {L |- sub U Q}**
============================
 {L |- sub S T}

Subgoal 1.4 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H2 H6 H4.
Subgoal 1.3:

Variables: Q L S T U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub Q T}
H5 : {L |- bound S U}**
H6 : {L |- sub U Q}**
H7 : {L |- sub U T}
============================
 {L |- sub S T}

Subgoal 1.4 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.4:

Variables: L T T2 S2 S1 T1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H4 : {L |- sub (arrow T1 T2) T}
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
============================
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H4.
Subgoal 1.4.1:

Variables: L T2 S2 S1 T1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
============================
 {L |- sub (arrow S1 S2) top}

Subgoal 1.4.2 is:
 {L |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 1.4.3 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.4.4 is:
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.4.2:

Variables: L T2 S2 S1 T1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- bound (arrow T1 T2) U}
============================
 {L |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 1.4.3 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.4.4 is:
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply bound_name to H2 H7.
Subgoal 1.4.2:

Variables: L T2 S2 S1 T1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- bound (arrow T1 T2) U}
H8 : name (arrow T1 T2)
============================
 {L |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 1.4.3 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.4.4 is:
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H8.
Subgoal 1.4.3:

Variables: L T T2 S2 S1 T1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- bound (arrow T1 T2) U}
H8 : {L |- sub U T}
============================
 {L |- sub (arrow S1 S2) T}

Subgoal 1.4.4 is:
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply bound_name to H2 H7.
Subgoal 1.4.3:

Variables: L T T2 S2 S1 T1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- bound (arrow T1 T2) U}
H8 : {L |- sub U T}
H9 : name (arrow T1 T2)
============================
 {L |- sub (arrow S1 S2) T}

Subgoal 1.4.4 is:
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H9.
Subgoal 1.4.4:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
============================
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H1.
Subgoal 1.4.4:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : ty T1 *
H10 : ty T2 *
============================
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply IH to H9.
Subgoal 1.4.4:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : ty T1 *
H10 : ty T2 *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
============================
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply IH to H10.
Subgoal 1.4.4:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : ty T1 *
H10 : ty T2 *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S T2} -> {L |- sub T2 T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X T2 :: L) -> {L |- sub P T2} ->
        {L, bound X T2 |- sub TM TN} -> {L, bound X P |- sub TM TN}
============================
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply H11 to H2 H7 H5.
Subgoal 1.4.4:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : ty T1 *
H10 : ty T2 *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S T2} -> {L |- sub T2 T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X T2 :: L) -> {L |- sub P T2} ->
        {L, bound X T2 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H15 : {L |- sub T4 S1}
============================
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply H13 to H2 H6 H8.
Subgoal 1.4.4:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : ty T1 *
H10 : ty T2 *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S T2} -> {L |- sub T2 T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X T2 :: L) -> {L |- sub P T2} ->
        {L, bound X T2 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H15 : {L |- sub T4 S1}
H16 : {L |- sub S2 T3}
============================
 {L |- sub (arrow S1 S2) (arrow T4 T3)}

Subgoal 1.4.5 is:
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.4.5:

Variables: L T T2 S2 S1 T1 F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L, [F] |- sub (arrow T1 T2) T}
H8 : member F L
============================
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply ctx_member to H2 H8.
Subgoal 1.4.5:

Variables: L T T2 S2 S1 T1 X U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (arrow T1 T2) @
IH1 : forall L S T, ctx L -> {L |- sub S (arrow T1 T2)}** ->
        {L |- sub (arrow T1 T2) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L |- sub S2 T2}**
H7 : {L, [bound X U] |- sub (arrow T1 T2) T}
H8 : member (bound X U) L
H9 : name X
============================
 {L |- sub (arrow S1 S2) T}

Subgoal 1.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H7.
Subgoal 1.5:

Variables: L T T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H4 : {L |- sub (all T1 (x\T2 x)) T}
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
============================
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H4.
Subgoal 1.5.1:

Variables: L T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
============================
 {L |- sub (all S1 (x\S2 x)) top}

Subgoal 1.5.2 is:
 {L |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 1.5.3 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.5.4 is:
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.5.2:

Variables: L T2 S2 T1 S1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- bound (all T1 (x\T2 x)) U}
============================
 {L |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 1.5.3 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.5.4 is:
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply bound_name to H2 H7.
Subgoal 1.5.2:

Variables: L T2 S2 T1 S1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- bound (all T1 (x\T2 x)) U}
H8 : name (all T1 (x\T2 x))
============================
 {L |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 1.5.3 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.5.4 is:
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H8.
Subgoal 1.5.3:

Variables: L T T2 S2 T1 S1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- bound (all T1 (x\T2 x)) U}
H8 : {L |- sub U T}
============================
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.5.4 is:
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply bound_name to H2 H7.
Subgoal 1.5.3:

Variables: L T T2 S2 T1 S1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- bound (all T1 (x\T2 x)) U}
H8 : {L |- sub U T}
H9 : name (all T1 (x\T2 x))
============================
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.5.4 is:
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H9.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H1.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply IH to H9.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply IH to H10.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S (T2 n1)} -> {L |- sub (T2 n1) T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X (T2 n1) :: L) ->
        {L |- sub P (T2 n1)} -> {L, bound X (T2 n1) |- sub TM TN} ->
        {L, bound X P |- sub TM TN}
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply H11 to H2 H7 H5.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S (T2 n1)} -> {L |- sub (T2 n1) T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X (T2 n1) :: L) ->
        {L |- sub P (T2 n1)} -> {L, bound X (T2 n1) |- sub TM TN} ->
        {L, bound X P |- sub TM TN}
H15 : {L |- sub T4 S1}
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply H12 to _ H7 H6 with X = n1.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S (T2 n1)} -> {L |- sub (T2 n1) T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X (T2 n1) :: L) ->
        {L |- sub P (T2 n1)} -> {L, bound X (T2 n1) |- sub TM TN} ->
        {L, bound X P |- sub TM TN}
H15 : {L |- sub T4 S1}
H16 : {L, bound n1 T4 |- sub (S2 n1) (T2 n1)}
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply H13 to _ H16 H8.
Subgoal 1.5.4:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L |- sub T4 T1}
H8 : {L, bound n1 T4 |- sub (T2 n1) (T3 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
H11 : forall L S T, ctx L -> {L |- sub S T1} -> {L |- sub T1 T} ->
        {L |- sub S T}
H12 : forall L P X TM TN, ctx (bound X T1 :: L) -> {L |- sub P T1} ->
        {L, bound X T1 |- sub TM TN} -> {L, bound X P |- sub TM TN}
H13 : forall L S T, ctx L -> {L |- sub S (T2 n1)} -> {L |- sub (T2 n1) T} ->
        {L |- sub S T}
H14 : forall L P X TM TN, ctx (bound X (T2 n1) :: L) ->
        {L |- sub P (T2 n1)} -> {L, bound X (T2 n1) |- sub TM TN} ->
        {L, bound X P |- sub TM TN}
H15 : {L |- sub T4 S1}
H16 : {L, bound n1 T4 |- sub (S2 n1) (T2 n1)}
H17 : {L, bound n1 T4 |- sub (S2 n1) (T3 n1)}
============================
 {L |- sub (all S1 (x\S2 x)) (all T4 (x\T3 x))}

Subgoal 1.5.5 is:
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 1.5.5:

Variables: L T T2 S2 T1 S1 F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L, [F] |- sub (all T1 (x\T2 x)) T}
H8 : member F L
============================
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply ctx_member to H2 H8.
Subgoal 1.5.5:

Variables: L T T2 S2 T1 S1 X U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty (all T1 (x\T2 x)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x\T2 x))}** ->
        {L |- sub (all T1 (x\T2 x)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : {L, [bound X U] |- sub (all T1 (x\T2 x)) T}
H8 : member (bound X U) L
H9 : name X
============================
 {L |- sub (all S1 (x\S2 x)) T}

Subgoal 1.6 is:
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H7.
Subgoal 1.6:

Variables: Q L S T F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub Q T}
H5 : {L, [F] |- sub S Q}**
H6 : member F L
============================
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < apply ctx_member to H2 H6.
Subgoal 1.6:

Variables: Q L S T X U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
IH1 : forall L S T, ctx L -> {L |- sub S Q}** -> {L |- sub Q T} ->
        {L |- sub S T}
H2 : ctx L
H4 : {L |- sub Q T}
H5 : {L, [bound X U] |- sub S Q}**
H6 : member (bound X U) L
H7 : name X
============================
 {L |- sub S T}

Subgoal 2 is:
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < case H5.
Subgoal 2:

Variables: Q
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
============================
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}

dual_theorem < induction on 3.
Subgoal 2:

Variables: Q
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
============================
 forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
   {L, bound X Q |- sub TM TN}@@ -> {L, bound X P |- sub TM TN}

dual_theorem < intros.
Subgoal 2:

Variables: Q L P X TM TN
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
============================
 {L, bound X P |- sub TM TN}

dual_theorem < case H5 (keep).
Subgoal 2.1:

Variables: Q L P X TM
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM top}@@
============================
 {L, bound X P |- sub TM top}

Subgoal 2.2 is:
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.2:

Variables: Q L P X TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H6 : {L, bound X Q |- bound TN U}**
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H6.
Subgoal 2.2:

Variables: Q L P X TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H7 : {L, bound X Q, [F] |- bound TN U}**
H8 : member F (bound X Q :: L)
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H8.
Subgoal 2.2.1:

Variables: Q L P X TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H7 : {L, bound X Q, [bound X Q] |- bound TN U}**
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.2.2 is:
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H7.
Subgoal 2.2.1:

Variables: L P TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty U @
H2 : forall L S T, ctx L -> {L |- sub S U} -> {L |- sub U T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X U :: L) -> {L |- sub P U} ->
        {L, bound X U |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound TN U :: L)
H4 : {L |- sub P U}
H5 : {L, bound TN U |- sub TN TN}@@
============================
 {L, bound TN P |- sub TN TN}

Subgoal 2.2.2 is:
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.2.2:

Variables: Q L P X TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H7 : {L, bound X Q, [F] |- bound TN U}**
H9 : member F L
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H3.
Subgoal 2.2.2:

Variables: Q L P X TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H7 : {L, bound X Q, [F] |- bound TN U}**
H9 : member F L
H10 : name X
H11 : ctx L
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply ctx_member to H11 H9.
Subgoal 2.2.2:

Variables: Q L P X TN U X1 U1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H7 : {L, bound X Q, [bound X1 U1] |- bound TN U}**
H9 : member (bound X1 U1) L
H10 : name X
H11 : ctx L
H12 : name X1
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H7.
Subgoal 2.2.2:

Variables: Q L P X TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TN TN}@@
H9 : member (bound TN U) L
H10 : name X
H11 : ctx L
H12 : name TN
============================
 {L, bound X P |- sub TN TN}

Subgoal 2.3 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.3:

Variables: Q L P X TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H6 : {L, bound X Q |- bound TM U}**
H7 : {L, bound X Q |- sub U TN}**
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H6.
Subgoal 2.3:

Variables: Q L P X TM TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H8 : {L, bound X Q, [F] |- bound TM U}**
H9 : member F (bound X Q :: L)
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H9.
Subgoal 2.3.1:

Variables: Q L P X TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H8 : {L, bound X Q, [bound X Q] |- bound TM U}**
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.3.2 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H8.
Subgoal 2.3.1:

Variables: L P TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty U @
H2 : forall L S T, ctx L -> {L |- sub S U} -> {L |- sub U T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X U :: L) -> {L |- sub P U} ->
        {L, bound X U |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound TM U :: L)
H4 : {L |- sub P U}
H5 : {L, bound TM U |- sub TM TN}@@
H7 : {L, bound TM U |- sub U TN}**
============================
 {L, bound TM P |- sub TM TN}

Subgoal 2.3.2 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H3 H4 H7.
Subgoal 2.3.1:

Variables: L P TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty U @
H2 : forall L S T, ctx L -> {L |- sub S U} -> {L |- sub U T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X U :: L) -> {L |- sub P U} ->
        {L, bound X U |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound TM U :: L)
H4 : {L |- sub P U}
H5 : {L, bound TM U |- sub TM TN}@@
H7 : {L, bound TM U |- sub U TN}**
H10 : {L, bound TM P |- sub U TN}
============================
 {L, bound TM P |- sub TM TN}

Subgoal 2.3.2 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H3.
Subgoal 2.3.1:

Variables: L P TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty U @
H2 : forall L S T, ctx L -> {L |- sub S U} -> {L |- sub U T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X U :: L) -> {L |- sub P U} ->
        {L, bound X U |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P U}
H5 : {L, bound TM U |- sub TM TN}@@
H7 : {L, bound TM U |- sub U TN}**
H10 : {L, bound TM P |- sub U TN}
H11 : name TM
H12 : ctx L
============================
 {L, bound TM P |- sub TM TN}

Subgoal 2.3.2 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply H2 to _ H4 H10.
Subgoal 2.3.1:

Variables: L P TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty U @
H2 : forall L S T, ctx L -> {L |- sub S U} -> {L |- sub U T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X U :: L) -> {L |- sub P U} ->
        {L, bound X U |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P U}
H5 : {L, bound TM U |- sub TM TN}@@
H7 : {L, bound TM U |- sub U TN}**
H10 : {L, bound TM P |- sub U TN}
H11 : name TM
H12 : ctx L
H13 : {L, bound TM P |- sub P TN}
============================
 {L, bound TM P |- sub TM TN}

Subgoal 2.3.2 is:
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.3.2:

Variables: Q L P X TM TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H8 : {L, bound X Q, [F] |- bound TM U}**
H10 : member F L
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H3 H4 H7.
Subgoal 2.3.2:

Variables: Q L P X TM TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H8 : {L, bound X Q, [F] |- bound TM U}**
H10 : member F L
H11 : {L, bound X P |- sub U TN}
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H3.
Subgoal 2.3.2:

Variables: Q L P X TM TN U F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H8 : {L, bound X Q, [F] |- bound TM U}**
H10 : member F L
H11 : {L, bound X P |- sub U TN}
H12 : name X
H13 : ctx L
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply ctx_member to H13 H10.
Subgoal 2.3.2:

Variables: Q L P X TM TN U X1 U1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H8 : {L, bound X Q, [bound X1 U1] |- bound TM U}**
H10 : member (bound X1 U1) L
H11 : {L, bound X P |- sub U TN}
H12 : name X
H13 : ctx L
H14 : name X1
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H8.
Subgoal 2.3.2:

Variables: Q L P X TM TN U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H7 : {L, bound X Q |- sub U TN}**
H10 : member (bound TM U) L
H11 : {L, bound X P |- sub U TN}
H12 : name X
H13 : ctx L
H14 : name TM
============================
 {L, bound X P |- sub TM TN}

Subgoal 2.4 is:
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.4:

Variables: Q L P X T2 S2 S1 T1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (arrow S1 S2) (arrow T1 T2)}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q |- sub S2 T2}**
============================
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H3 H4 H6.
Subgoal 2.4:

Variables: Q L P X T2 S2 S1 T1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (arrow S1 S2) (arrow T1 T2)}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q |- sub S2 T2}**
H8 : {L, bound X P |- sub T1 S1}
============================
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H3 H4 H7.
Subgoal 2.4:

Variables: Q L P X T2 S2 S1 T1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (arrow S1 S2) (arrow T1 T2)}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q |- sub S2 T2}**
H8 : {L, bound X P |- sub T1 S1}
H9 : {L, bound X P |- sub S2 T2}
============================
 {L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.5:

Variables: Q L P X T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
============================
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H3 H4 H6.
Subgoal 2.5:

Variables: Q L P X T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H8 : {L, bound X P |- sub T1 S1}
============================
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < assert ctx (bound X Q :: bound n1 T1 :: L).
Subgoal 2.5.1:

Variables: Q L P X T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H8 : {L, bound X P |- sub T1 S1}
============================
 ctx (bound X Q :: bound n1 T1 :: L)

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < case H3.
Subgoal 2.5.1:

Variables: Q L P X T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H8 : {L, bound X P |- sub T1 S1}
H9 : name X
H10 : ctx L
============================
 ctx (bound X Q :: bound n1 T1 :: L)

Subgoal 2.5 is:
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.5:

Variables: Q L P X T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H8 : {L, bound X P |- sub T1 S1}
H9 : ctx (bound X Q :: bound n1 T1 :: L)
============================
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < apply IH1 to H9 H4 H7.
Subgoal 2.5:

Variables: Q L P X T2 S2 T1 S1
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}@@
H6 : {L, bound X Q |- sub T1 S1}**
H7 : {L, bound X Q, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H8 : {L, bound X P |- sub T1 S1}
H9 : ctx (bound X Q :: bound n1 T1 :: L)
H10 : {L, bound n1 T1, bound X P |- sub (S2 n1) (T2 n1)}
============================
 {L, bound X P |- sub (all S1 (x\S2 x)) (all T1 (x\T2 x))}

Subgoal 2.6 is:
 {L, bound X P |- sub TM TN}

dual_theorem < search.
Subgoal 2.6:

Variables: Q L P X TM TN F
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H6 : {L, bound X Q, [F] |- sub TM TN}**
H7 : member F (bound X Q :: L)
============================
 {L, bound X P |- sub TM TN}

dual_theorem < apply ctx_member to H3 H7.
Subgoal 2.6:

Variables: Q L P X TM TN X1 U
IH : forall Q, ty Q * ->
       (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
            {L |- sub S T}) /\
       (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
            {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN})
H1 : ty Q @
H2 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
IH1 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
        {L, bound X Q |- sub TM TN}** -> {L, bound X P |- sub TM TN}
H3 : ctx (bound X Q :: L)
H4 : {L |- sub P Q}
H5 : {L, bound X Q |- sub TM TN}@@
H6 : {L, bound X Q, [bound X1 U] |- sub TM TN}**
H7 : member (bound X1 U) (bound X Q :: L)
H8 : name X1
============================
 {L, bound X P |- sub TM TN}

dual_theorem < case H6.
Proof completed.
Abella < Theorem transitivity : 
forall L Q S T, ctx L -> ty Q -> {L |- sub S Q} -> {L |- sub Q T} ->
  {L |- sub S T}.


============================
 forall L Q S T, ctx L -> ty Q -> {L |- sub S Q} -> {L |- sub Q T} ->
   {L |- sub S T}

transitivity < intros.

Variables: L Q S T
H1 : ctx L
H2 : ty Q
H3 : {L |- sub S Q}
H4 : {L |- sub Q T}
============================
 {L |- sub S T}

transitivity < apply dual_theorem to H2.

Variables: L Q S T
H1 : ctx L
H2 : ty Q
H3 : {L |- sub S Q}
H4 : {L |- sub Q T}
H5 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
H6 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
       {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}
============================
 {L |- sub S T}

transitivity < apply H5 to H1 H3 H4.

Variables: L Q S T
H1 : ctx L
H2 : ty Q
H3 : {L |- sub S Q}
H4 : {L |- sub Q T}
H5 : forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} ->
       {L |- sub S T}
H6 : forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} ->
       {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}
H7 : {L |- sub S T}
============================
 {L |- sub S T}

transitivity < search.
Proof completed.
Abella <