Welcome to Abella 1.1.3-dev2
Reading clauses from poplmark-1a.mod
Abella < Define nabla x, name x.
Abella < Define ctx nil.
Abella < Define ctx (bound X U :: L) := name X /\ ctx L.
Abella < Define cty L top.
Abella < Define cty L X := exists U, member (bound X U) L.
Abella < Define cty L (arrow T1 T2) := cty L T1 /\ cty L T2.
Abella < Define cty L (all T1 T2) := cty L T1 /\ (nabla x, cty (bound x T1 :: L) (T2 x)).
Abella < Define ty top.
Abella < Define nabla x, ty x.
Abella < Define ty (arrow T1 T2) := ty T1 /\ ty T2.
Abella < Define 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}.
1 subgoal(s).
============================
forall L T, cty L T -> {L |- sub T T}
sub_refl < induction on 1.
1 subgoal(s).
IH : forall L T, cty L T * -> {L |- sub T T}
============================
forall L T, cty L T @ -> {L |- sub T T}
sub_refl < intros.
1 subgoal(s).
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.
4 subgoal(s).
Variables: L, T
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.
3 subgoal(s).
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 2 is:
{L |- sub (arrow T1 T2) (arrow T1 T2)}
subgoal 3 is:
{L |- sub (all T1 T2) (all T1 T2)}
sub_refl < search.
2 subgoal(s).
Variables: L, T, 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 2 is:
{L |- sub (all T1 T2) (all T1 T2)}
sub_refl < apply IH to H2.
2 subgoal(s).
Variables: L, T, 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 2 is:
{L |- sub (all T1 T2) (all T1 T2)}
sub_refl < apply IH to H3.
2 subgoal(s).
Variables: L, T, 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 2 is:
{L |- sub (all T1 T2) (all T1 T2)}
sub_refl < search.
1 subgoal(s).
Variables: L, T, 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.
1 subgoal(s).
Variables: L, T, 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.
1 subgoal(s).
Variables: L, T, 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_sub_absurd :
forall S T L, ctx L -> member (sub S T) L -> false.
1 subgoal(s).
============================
forall S T L, ctx L -> member (sub S T) L -> false
ctx_sub_absurd < induction on 1.
1 subgoal(s).
IH : forall S T L, ctx L * -> member (sub S T) L -> false
============================
forall S T L, ctx L @ -> member (sub S T) L -> false
ctx_sub_absurd < intros.
1 subgoal(s).
Variables: S, T, L
IH : forall S T L, ctx L * -> member (sub S T) L -> false
H1 : ctx L @
H2 : member (sub S T) L
============================
false
ctx_sub_absurd < case H1.
2 subgoal(s).
Variables: S, T, L
IH : forall S T L, ctx L * -> member (sub S T) L -> false
H2 : member (sub S T) nil
============================
false
subgoal 2 is:
false
ctx_sub_absurd < case H2.
1 subgoal(s).
Variables: S, T, L, L1, U, X
IH : forall S T L, ctx L * -> member (sub S T) L -> false
H2 : member (sub S T) (bound X U :: L1)
H3 : name X
H4 : ctx L1 *
============================
false
ctx_sub_absurd < case H2.
1 subgoal(s).
Variables: S, T, L, L1, U, X
IH : forall S T L, ctx L * -> member (sub S T) L -> false
H3 : name X
H4 : ctx L1 *
H5 : member (sub S T) L1
============================
false
ctx_sub_absurd < apply IH to H4 H5.
Proof completed.
Abella < Theorem ctx_name :
forall L X U, ctx L -> member (bound X U) L -> name X.
1 subgoal(s).
============================
forall L X U, ctx L -> member (bound X U) L -> name X
ctx_name < induction on 1.
1 subgoal(s).
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
============================
forall L X U, ctx L @ -> member (bound X U) L -> name X
ctx_name < intros.
1 subgoal(s).
Variables: L, X, U
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H1 : ctx L @
H2 : member (bound X U) L
============================
name X
ctx_name < case H1.
2 subgoal(s).
Variables: L, X, U
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H2 : member (bound X U) nil
============================
name X
subgoal 2 is:
name X
ctx_name < case H2.
1 subgoal(s).
Variables: L, X, U, L1, U1, X1
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H2 : member (bound X U) (bound X1 U1 :: L1)
H3 : name X1
H4 : ctx L1 *
============================
name X
ctx_name < case H2.
2 subgoal(s).
Variables: L, X, U, L1, U1, X1
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H3 : name X1
H4 : ctx L1 *
============================
name X1
subgoal 2 is:
name X
ctx_name < case H3.
2 subgoal(s).
Variables: L, X, U, L1, U1, X1
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H4 : ctx (L1 n1) *
============================
name n1
subgoal 2 is:
name X
ctx_name < search.
1 subgoal(s).
Variables: L, X, U, L1, U1, X1
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H3 : name X1
H4 : ctx L1 *
H5 : member (bound X U) L1
============================
name X
ctx_name < apply IH to H4 H5.
1 subgoal(s).
Variables: L, X, U, L1, U1, X1
IH : forall L X U, ctx L * -> member (bound X U) L -> name X
H3 : name X1
H4 : ctx L1 *
H5 : member (bound X U) L1
H6 : name X
============================
name X
ctx_name < search.
Proof completed.
Abella < Theorem bound_name :
forall L X U, ctx L -> {L |- bound X U} -> name X.
1 subgoal(s).
============================
forall L X U, ctx L -> {L |- bound X U} -> name X
bound_name < intros.
1 subgoal(s).
Variables: L, X, U
H1 : ctx L
H2 : {L |- bound X U}
============================
name X
bound_name < case H2.
1 subgoal(s).
Variables: L, X, U
H1 : ctx L
H3 : member (bound X U) L
============================
name X
bound_name < apply ctx_name to H1 H3.
1 subgoal(s).
Variables: L, X, U
H1 : ctx L
H3 : member (bound X U) L
H4 : name X
============================
name X
bound_name < search.
Proof completed.
Abella < Theorem sub_top :
forall L T, ctx L -> {L |- sub top T} -> T = top.
1 subgoal(s).
============================
forall L T, ctx L -> {L |- sub top T} -> T = top
sub_top < intros.
1 subgoal(s).
Variables: L, T
H1 : ctx L
H2 : {L |- sub top T}
============================
T = top
sub_top < case H2.
4 subgoal(s).
Variables: L, T
H1 : ctx L
H3 : member (sub top T) L
============================
T = top
subgoal 2 is:
top = top
subgoal 3 is:
top = top
subgoal 4 is:
T = top
sub_top < apply ctx_sub_absurd to H1 H3.
3 subgoal(s).
Variables: L, T
H1 : ctx L
============================
top = top
subgoal 2 is:
top = top
subgoal 3 is:
T = top
sub_top < search.
2 subgoal(s).
Variables: L, T, U
H1 : ctx L
H3 : {L |- bound top U}
============================
top = top
subgoal 2 is:
T = top
sub_top < search.
1 subgoal(s).
Variables: L, T, U
H1 : ctx L
H3 : {L |- bound top U}
H4 : {L |- sub U T}
============================
T = top
sub_top < apply bound_name to H1 H3.
1 subgoal(s).
Variables: L, T, U
H1 : ctx L
H3 : {L |- bound top U}
H4 : {L |- sub U T}
H5 : name top
============================
T = top
sub_top < case H5.
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}).
1 subgoal(s).
============================
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.
1 subgoal(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})
============================
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.
1 subgoal(s).
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*.
2 subgoal(s).
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.
2 subgoal(s).
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.
2 subgoal(s).
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.
7 subgoal(s).
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
H4 : {L |- sub Q T}
H5 : member (sub S Q) L
============================
{L |- sub S T}
subgoal 2 is:
{L |- sub S T}
subgoal 3 is:
{L |- sub Q T}
subgoal 4 is:
{L |- sub S T}
subgoal 5 is:
{L |- sub (arrow S1 S2) T}
subgoal 6 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 7 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_sub_absurd to H2 H5.
6 subgoal(s).
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 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 2 is:
{L |- sub Q T}
subgoal 3 is:
{L |- sub S T}
subgoal 4 is:
{L |- sub (arrow S1 S2) T}
subgoal 5 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 6 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.
6 subgoal(s).
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 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 2 is:
{L |- sub Q T}
subgoal 3 is:
{L |- sub S T}
subgoal 4 is:
{L |- sub (arrow S1 S2) T}
subgoal 5 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 6 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.
5 subgoal(s).
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 Q U}**
============================
{L |- sub Q T}
subgoal 2 is:
{L |- sub S T}
subgoal 3 is:
{L |- sub (arrow S1 S2) T}
subgoal 4 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 5 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.
4 subgoal(s).
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 2 is:
{L |- sub (arrow S1 S2) T}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 4 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.
4 subgoal(s).
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 2 is:
{L |- sub (arrow S1 S2) T}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 4 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
7 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 : member (sub (arrow T1 T2) T) L
============================
{L |- sub (arrow S1 S2) T}
subgoal 2 is:
{L |- sub (arrow S1 S2) top}
subgoal 3 is:
{L |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L |- sub (arrow S1 S2) T}
subgoal 5 is:
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 6 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 7 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_sub_absurd to H2 H7.
6 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 2 is:
{L |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 3 is:
{L |- sub (arrow S1 S2) T}
subgoal 4 is:
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 5 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 6 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.
5 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 2 is:
{L |- sub (arrow S1 S2) T}
subgoal 3 is:
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 4 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 5 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.
5 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 2 is:
{L |- sub (arrow S1 S2) T}
subgoal 3 is:
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 4 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 5 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.
4 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 2 is:
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 4 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.
4 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (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 2 is:
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 4 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 T3 T1}
H8 : {L |- sub T2 T4}
============================
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 T3 T1}
H8 : {L |- sub T2 T4}
H9 : ty T1 *
H10 : ty T2 *
============================
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 T3 T1}
H8 : {L |- sub T2 T4}
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 T3 T4)}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 T3 T1}
H8 : {L |- sub T2 T4}
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 T3 T4)}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 T3 T1}
H8 : {L |- sub T2 T4}
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 T3 S1}
============================
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 T3 T1}
H8 : {L |- sub T2 T4}
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 T3 S1}
H16 : {L |- sub S2 T4}
============================
{L |- sub (arrow S1 S2) (arrow T3 T4)}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) T} -> {L |- sub S T}
H2 : ctx L
H4 : {L |- sub (all T1 (x1\T2 x1)) T}
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
============================
{L |- sub (all S1 (x1\S2 x1)) 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.
6 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) T} -> {L |- sub S T}
H2 : ctx L
H5 : {L |- sub T1 S1}**
H6 : {L, bound n1 T1 |- sub (S2 n1) (T2 n1)}**
H7 : member (sub (all T1 (x1\T2 x1)) T) L
============================
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) top}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
subgoal 4 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 5 is:
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
subgoal 6 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_sub_absurd to H2 H7.
5 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 (x1\S2 x1)) top}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 4 is:
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
subgoal 5 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.
4 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 (x1\T2 x1)) U}
============================
{L |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
subgoal 4 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.
4 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 (x1\T2 x1)) U}
H8 : name (all T1 (x1\T2 x1))
============================
{L |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 3 is:
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
subgoal 4 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 (x1\T2 x1)) U}
H8 : {L |- sub U T}
============================
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
subgoal 3 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.
3 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, 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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 (x1\T2 x1)) U}
H8 : {L |- sub U T}
H9 : name (all T1 (x1\T2 x1))
============================
{L |- sub (all S1 (x1\S2 x1)) T}
subgoal 2 is:
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
subgoal 3 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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1)) @
IH1 : forall L S T, ctx L -> {L |- sub S (all T1 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 n1)}
============================
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 n1)}
H9 : ty T1 *
H10 : ty (T2 n1) *
============================
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 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 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 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 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 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 T3 S1}
============================
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 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 T3 S1}
H16 : {L, bound n1 T3 |- sub (S2 n1) (T2 n1)}
============================
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
2 subgoal(s).
Variables: Q, L, S, T, T2, T1, S2, S1, T4, T3
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 (x1\T2 x1))}** ->
{L |- sub (all T1 (x1\T2 x1)) 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 T3 T1}
H8 : {L, bound n1 T3 |- sub (T2 n1) (T4 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 T3 S1}
H16 : {L, bound n1 T3 |- sub (S2 n1) (T2 n1)}
H17 : {L, bound n1 T3 |- sub (S2 n1) (T4 n1)}
============================
{L |- sub (all S1 (x1\S2 x1)) (all T3 (x1\T4 x1))}
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.
1 subgoal(s).
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.
1 subgoal(s).
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.
1 subgoal(s).
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).
6 subgoal(s).
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}@@
H6 : member (sub TM TN) (bound X Q :: L)
============================
{L, bound X P |- sub TM TN}
subgoal 2 is:
{L, bound X P |- sub TM top}
subgoal 3 is:
{L, bound X P |- sub TN TN}
subgoal 4 is:
{L, bound X P |- sub TM TN}
subgoal 5 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 6 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply ctx_sub_absurd to H3 H6.
5 subgoal(s).
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 top}@@
============================
{L, bound X P |- sub TM top}
subgoal 2 is:
{L, bound X P |- sub TN TN}
subgoal 3 is:
{L, bound X P |- sub TM TN}
subgoal 4 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 5 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
4 subgoal(s).
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 TN TN}@@
H6 : {L, bound X Q |- bound TN U}**
============================
{L, bound X P |- sub TN TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < case H6.
4 subgoal(s).
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 TN TN}@@
H7 : member (bound TN U) (bound X Q :: L)
============================
{L, bound X P |- sub TN TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < case H7.
5 subgoal(s).
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 X X}@@
============================
{L, bound X P |- sub X X}
subgoal 2 is:
{L, bound X P |- sub TN TN}
subgoal 3 is:
{L, bound X P |- sub TM TN}
subgoal 4 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 5 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
4 subgoal(s).
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 TN TN}@@
H8 : member (bound TN U) L
============================
{L, bound X P |- sub TN TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
3 subgoal(s).
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 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 3 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < case H6.
3 subgoal(s).
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 : member (bound TM U) (bound X Q :: L)
============================
{L, bound X P |- sub TM TN}
subgoal 2 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 3 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < case H8.
4 subgoal(s).
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 X TN}@@
H7 : {L, bound X Q |- sub Q TN}**
============================
{L, bound X P |- sub X TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply IH1 to H3 H4 H7.
4 subgoal(s).
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 X TN}@@
H7 : {L, bound X Q |- sub Q TN}**
H9 : {L, bound X P |- sub Q TN}
============================
{L, bound X P |- sub X TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < case H3.
4 subgoal(s).
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 X TN}@@
H7 : {L, bound X Q |- sub Q TN}**
H9 : {L, bound X P |- sub Q TN}
H10 : name X
H11 : ctx L
============================
{L, bound X P |- sub X TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply H2 to _ H4 H9.
4 subgoal(s).
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 X TN}@@
H7 : {L, bound X Q |- sub Q TN}**
H9 : {L, bound X P |- sub Q TN}
H10 : name X
H11 : ctx L
H12 : {L, bound X P |- sub P TN}
============================
{L, bound X P |- sub X TN}
subgoal 2 is:
{L, bound X P |- sub TM TN}
subgoal 3 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 4 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
3 subgoal(s).
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}**
H9 : member (bound TM U) L
============================
{L, bound X P |- sub TM TN}
subgoal 2 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 3 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply IH1 to H3 H4 H7.
3 subgoal(s).
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}**
H9 : member (bound TM U) L
H10 : {L, bound X P |- sub U TN}
============================
{L, bound X P |- sub TM TN}
subgoal 2 is:
{L, bound X P |- sub (arrow S1 S2) (arrow T1 T2)}
subgoal 3 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
2 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (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 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply IH1 to H3 H4 H6.
2 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (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 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply IH1 to H3 H4 H7.
2 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (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 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
1 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (x1\S2 x1)) (all T1 (x1\T2 x1))}@@
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 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply IH1 to H3 H4 H6.
1 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (x1\S2 x1)) (all T1 (x1\T2 x1))}@@
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 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < assert ctx (bound X Q :: bound n1 T1 :: L).
2 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (x1\S2 x1)) (all T1 (x1\T2 x1))}@@
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 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < case H3.
2 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (x1\S2 x1)) (all T1 (x1\T2 x1))}@@
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 is:
{L, bound X P |- sub (all S1 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
1 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (x1\S2 x1)) (all T1 (x1\T2 x1))}@@
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 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < apply IH1 to H9 H4 H7.
1 subgoal(s).
Variables: Q, L, P, X, TM, TN, T2, T1, S2, 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 (x1\S2 x1)) (all T1 (x1\T2 x1))}@@
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 (x1\S2 x1)) (all T1 (x1\T2 x1))}
dual_theorem < search.
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}.
1 subgoal(s).
============================
forall L Q S T, ctx L -> ty Q -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
transitivity < intros.
1 subgoal(s).
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.
1 subgoal(s).
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.
1 subgoal(s).
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 < Goodbye.
