Welcome to Abella 2.0.5-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 <
