Welcome to Abella 2.0.5-dev.
Abella < Specification "fsub".


Abella < Define name : tp -> prop by
nabla n, name n.


Abella < Define ctx : olist -> prop by
ctx nil;
nabla a, ctx (sub a a :: sub a T :: (pi U\pi V\sub a U => sub U V => sub a V) :: L) := ctx L.


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


Abella < Theorem ctx_mem :
forall L F, ctx L -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V)).



============================
forall L F, ctx L -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))

ctx_mem < induction on 1.


IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
============================
forall L F, ctx L @ -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))

ctx_mem < intros.


Variables: L F
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H1 : ctx L @
H2 : member F L
============================
exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < case H1.

Subgoal 1:

Variables: F
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H2 : member F nil
============================
exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V)

Subgoal 2 is:
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < case H2.

Subgoal 2:

Variables: F L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H2 : member (F n1)
(sub n1 n1 :: sub n1 T ::
(pi U\pi V\sub n1 U => sub U V => sub n1 V) :: L1)
H3 : ctx L1 *
============================
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < case H2.

Subgoal 2.1:

Variables: L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
============================
exists A, name A /\
(sub n1 n1 = sub A A \/ (exists T, sub n1 n1 = sub A T) \/ sub n1 n1 =
pi U\pi V\sub A U => sub U V => sub A V)

Subgoal 2.2 is:
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < search.

Subgoal 2.2:

Variables: F L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
H4 : member (F n1)
(sub n1 T :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) :: L1)
============================
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < case H4.

Subgoal 2.2.1:

Variables: L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
============================
exists A, name A /\
(sub n1 T = sub A A \/ (exists T1, sub n1 T = sub A T1) \/ sub n1 T =
pi U\pi V\sub A U => sub U V => sub A V)

Subgoal 2.2.2 is:
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < search.

Subgoal 2.2.2:

Variables: F L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
H5 : member (F n1) ((pi U\pi V\sub n1 U => sub U V => sub n1 V) :: L1)
============================
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < case H5.

Subgoal 2.2.2.1:

Variables: L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
============================
exists A, name A /\
(pi U\pi V\sub n1 U => sub U V => sub n1 V = sub A A \/
(exists T, pi U\pi V\sub n1 U => sub U V => sub n1 V = sub A T) \/
pi U\pi V\sub n1 U => sub U V => sub n1 V =
pi U\pi V\sub A U => sub U V => sub A V)

Subgoal 2.2.2.2 is:
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < search.

Subgoal 2.2.2.2:

Variables: F L1 T
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
H6 : member (F n1) L1
============================
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < apply IH to H3 H6.

Subgoal 2.2.2.2:

Variables: F L1 T A
IH : forall L F, ctx L * -> member F L ->
(exists A, name A /\
(F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V))
H3 : ctx L1 *
H6 : member (F n1) L1
H7 : name (A n1)
H8 : F n1 = sub (A n1) (A n1) \/ (exists T, F n1 = sub (A n1) T) \/ F n1 =
pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V
============================
exists A, name A /\
(F n1 = sub A A \/ (exists T, F n1 = sub A T) \/ F n1 =
pi U\pi V\sub A U => sub U V => sub A V)

ctx_mem < search.
Proof completed.

Abella < Theorem ctx_sync :
forall A L T, ctx L -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L.



============================
forall A L T, ctx L -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L

ctx_sync < induction on 1.


IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
============================
forall A L T, ctx L @ -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L

ctx_sync < intros.


Variables: A L T
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H1 : ctx L @
H2 : member (sub A T) L
============================
member (pi U\pi V\sub A U => sub U V => sub A V) L

ctx_sync < case H1.

Subgoal 1:

Variables: A T
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H2 : member (sub A T) nil
============================
member (pi U\pi V\sub A U => sub U V => sub A V) nil

Subgoal 2 is:
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < case H2.

Subgoal 2:

Variables: A T L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H2 : member (sub (A n1) (T n1))
(sub n1 n1 :: sub n1 T1 ::
(pi U\pi V\sub n1 U => sub U V => sub n1 V) :: L1)
H3 : ctx L1 *
============================
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < case H2.

Subgoal 2.1:

Variables: L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : ctx L1 *
============================
member (pi U\pi V\sub n1 U => sub U V => sub n1 V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

Subgoal 2.2 is:
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < search.

Subgoal 2.2:

Variables: A T L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : ctx L1 *
H4 : member (sub (A n1) (T n1))
(sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) :: L1)
============================
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < case H4.

Subgoal 2.2.1:

Variables: L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : ctx L1 *
============================
member (pi U\pi V\sub n1 U => sub U V => sub n1 V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

Subgoal 2.2.2 is:
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < search.

Subgoal 2.2.2:

Variables: A T L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : ctx L1 *
H5 : member (sub (A n1) (T n1))
((pi U\pi V\sub n1 U => sub U V => sub n1 V) :: L1)
============================
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < case H5.

Subgoal 2.2.2:

Variables: A T L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : ctx L1 *
H6 : member (sub (A n1) (T n1)) L1
============================
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < apply IH to H3 H6.

Subgoal 2.2.2:

Variables: A T L1 T1
IH : forall A L T, ctx L * -> member (sub A T) L ->
member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : ctx L1 *
H6 : member (sub (A n1) (T n1)) L1
H7 : member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V) L1
============================
member (pi U\pi V\sub (A n1) U => sub U V => sub (A n1) V)
(sub n1 n1 :: sub n1 T1 :: (pi U\pi V\sub n1 U => sub U V => sub n1 V) ::
L1)

ctx_sync < search.
Proof completed.

Abella < Theorem ctx_sub_name :
forall L D G, ctx L -> member D L -> {L, [D] |- G} ->
(exists A T, G = sub A T /\ name A).



============================
forall L D G, ctx L -> member D L -> {L, [D] |- G} ->
(exists A T, G = sub A T /\ name A)

ctx_sub_name < intros.


Variables: L D G
H1 : ctx L
H2 : member D L
H3 : {L, [D] |- G}
============================
exists A T, G = sub A T /\ name A

ctx_sub_name < apply ctx_mem to H1 H2.


Variables: L D G A
H1 : ctx L
H2 : member D L
H3 : {L, [D] |- G}
H4 : name A
H5 : D = sub A A \/ (exists T, D = sub A T) \/ D =
pi U\pi V\sub A U => sub U V => sub A V
============================
exists A T, G = sub A T /\ name A

ctx_sub_name < case H5.

Subgoal 1:

Variables: L G A
H1 : ctx L
H2 : member (sub A A) L
H3 : {L, [sub A A] |- G}
H4 : name A
============================
exists A T, G = sub A T /\ name A

Subgoal 2 is:
exists A T, G = sub A T /\ name A

Subgoal 3 is:
exists A T, G = sub A T /\ name A

ctx_sub_name < case H3.

Subgoal 1:

Variables: L A
H1 : ctx L
H2 : member (sub A A) L
H4 : name A
============================
exists A1 T, sub A A = sub A1 T /\ name A1

Subgoal 2 is:
exists A T, G = sub A T /\ name A

Subgoal 3 is:
exists A T, G = sub A T /\ name A

ctx_sub_name < search.

Subgoal 2:

Variables: L G A T
H1 : ctx L
H2 : member (sub A T) L
H3 : {L, [sub A T] |- G}
H4 : name A
============================
exists A T, G = sub A T /\ name A

Subgoal 3 is:
exists A T, G = sub A T /\ name A

ctx_sub_name < case H3.

Subgoal 2:

Variables: L A T
H1 : ctx L
H2 : member (sub A T) L
H4 : name A
============================
exists A1 T1, sub A T = sub A1 T1 /\ name A1

Subgoal 3 is:
exists A T, G = sub A T /\ name A

ctx_sub_name < search.

Subgoal 3:

Variables: L G A
H1 : ctx L
H2 : member (pi U\pi V\sub A U => sub U V => sub A V) L
H3 : {L, [pi U\pi V\sub A U => sub U V => sub A V] |- G}
H4 : name A
============================
exists A T, G = sub A T /\ name A

ctx_sub_name < case H3.

Subgoal 3:

Variables: L A V U
H1 : ctx L
H2 : member (pi U\pi V\sub A U => sub U V => sub A V) L
H4 : name A
H6 : {L |- sub A U}
H7 : {L |- sub U V}
============================
exists A1 T, sub A V = sub A1 T /\ name A1

ctx_sub_name < search.
Proof completed.

Abella < Theorem transitivity :
forall L S Q T, ctx L -> tp Q -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}.



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

transitivity < induction on 2.


IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
============================
forall L S Q T, ctx L -> tp Q @ -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}

transitivity < intros.


Variables: L S Q T
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H3 : {L |- sub S Q}
H4 : {L |- sub Q T}
============================
{L |- sub S T}

transitivity < case H3.

Subgoal 1:

Variables: L S T
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp top @
H4 : {L |- sub top T}
============================
{L |- sub S T}

Subgoal 2 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < case H4.

Subgoal 1.1:

Variables: L S
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp top @
============================
{L |- sub S top}

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

Subgoal 2 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < search.

Subgoal 1.2:

Variables: L S T F
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp top @
H5 : {L, [F] |- sub top T}
H6 : member F L
============================
{L |- sub S T}

Subgoal 2 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < apply ctx_sub_name to H1 H6 H5.

Subgoal 1.2:

Variables: L S F T1
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp top @
H5 : {L, [F] |- sub top T1}
H6 : member F L
H7 : name top
============================
{L |- sub S T1}

Subgoal 2 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < case H7.

Subgoal 2:

Variables: L T T2 S2 S1 T1
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (arr T1 T2) @
H4 : {L |- sub (arr T1 T2) T}
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
============================
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < case H4.

Subgoal 2.1:

Variables: L T2 S2 S1 T1
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (arr T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
============================
{L |- sub (arr S1 S2) top}

Subgoal 2.2 is:
{L |- sub (arr S1 S2) (arr T4 T3)}

Subgoal 2.3 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < search.

Subgoal 2.2:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (arr T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
============================
{L |- sub (arr S1 S2) (arr T4 T3)}

Subgoal 2.3 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < case H2.

Subgoal 2.2:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : tp T1 *
H10 : tp T2 *
============================
{L |- sub (arr S1 S2) (arr T4 T3)}

Subgoal 2.3 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < apply IH to H1 H9 H7 H5.

Subgoal 2.2:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : tp T1 *
H10 : tp T2 *
H11 : {L |- sub T4 S1}
============================
{L |- sub (arr S1 S2) (arr T4 T3)}

Subgoal 2.3 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < apply IH to H1 H10 H6 H8.

Subgoal 2.2:

Variables: L T2 S2 S1 T1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
H7 : {L |- sub T4 T1}
H8 : {L |- sub T2 T3}
H9 : tp T1 *
H10 : tp T2 *
H11 : {L |- sub T4 S1}
H12 : {L |- sub S2 T3}
============================
{L |- sub (arr S1 S2) (arr T4 T3)}

Subgoal 2.3 is:
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < search.

Subgoal 2.3:

Variables: L T T2 S2 S1 T1 F
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (arr T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
H7 : {L, [F] |- sub (arr T1 T2) T}
H8 : member F L
============================
{L |- sub (arr S1 S2) T}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < apply ctx_sub_name to H1 H8 H7.

Subgoal 2.3:

Variables: L T2 S2 S1 T1 F T3
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (arr T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L |- sub S2 T2}
H7 : {L, [F] |- sub (arr T1 T2) T3}
H8 : member F L
H9 : name (arr T1 T2)
============================
{L |- sub (arr S1 S2) T3}

Subgoal 3 is:
{L |- sub (all S1 S2) T}

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

transitivity < case H9.

Subgoal 3:

Variables: L T T2 S2 T1 S1
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (all T1 T2) @
H4 : {L |- sub (all T1 T2) T}
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
============================
{L |- sub (all S1 S2) T}

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

transitivity < case H4.

Subgoal 3.1:

Variables: L T2 S2 T1 S1
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (all T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
============================
{L |- sub (all S1 S2) top}

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

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < search.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (all T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < case H2.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
H9 : tp T1 *
H10 : tp (T2 n1) *
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < apply IH to H1 H9 H7 H5.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
H9 : tp T1 *
H10 : tp (T2 n1) *
H11 : {L |- sub T4 S1}
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < assert {pi U\pi V\sub n1 U => sub U V => sub n1 V, sub T4 T1, sub n1 T4 |-
sub n1 T1}.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
H9 : tp T1 *
H10 : tp (T2 n1) *
H11 : {L |- sub T4 S1}
H12 : {pi U\pi V\sub n1 U => sub U V => sub n1 V, sub T4 T1, sub n1 T4 |-
sub n1 T1}
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < cut H12 with H7.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
H9 : tp T1 *
H10 : tp (T2 n1) *
H11 : {L |- sub T4 S1}
H12 : {pi U\pi V\sub n1 U => sub U V => sub n1 V, sub T4 T1, sub n1 T4 |-
sub n1 T1}
H13 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4 |- sub n1 T1}
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < cut H6 with H13.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
H9 : tp T1 *
H10 : tp (T2 n1) *
H11 : {L |- sub T4 S1}
H12 : {pi U\pi V\sub n1 U => sub U V => sub n1 V, sub T4 T1, sub n1 T4 |-
sub n1 T1}
H13 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4 |- sub n1 T1}
H14 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < apply IH to _ H10 H14 H8.

Subgoal 3.2:

Variables: L T2 S2 T1 S1 T3 T4
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L |- sub T4 T1}
H8 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (T2 n1) (T3 n1)}
H9 : tp T1 *
H10 : tp (T2 n1) *
H11 : {L |- sub T4 S1}
H12 : {pi U\pi V\sub n1 U => sub U V => sub n1 V, sub T4 T1, sub n1 T4 |-
sub n1 T1}
H13 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4 |- sub n1 T1}
H14 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H15 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T4, sub n1 n1 |-
sub (S2 n1) (T3 n1)}
============================
{L |- sub (all S1 S2) (all T4 T3)}

Subgoal 3.3 is:
{L |- sub (all S1 S2) T}

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

transitivity < search.

Subgoal 3.3:

Variables: L T T2 S2 T1 S1 F
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (all T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L, [F] |- sub (all T1 T2) T}
H8 : member F L
============================
{L |- sub (all S1 S2) T}

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

transitivity < apply ctx_sub_name to H1 H8 H7.

Subgoal 3.3:

Variables: L T2 S2 T1 S1 F T3
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp (all T1 T2) @
H5 : {L |- sub T1 S1}
H6 : {L, pi U\pi V\sub n1 U => sub U V => sub n1 V, sub n1 T1, sub n1 n1 |-
sub (S2 n1) (T2 n1)}
H7 : {L, [F] |- sub (all T1 T2) T3}
H8 : member F L
H9 : name (all T1 T2)
============================
{L |- sub (all S1 S2) T3}

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

transitivity < case H9.

Subgoal 4:

Variables: L S Q T F
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H5 : {L, [F] |- sub S Q}
H6 : member F L
============================
{L |- sub S T}

transitivity < apply ctx_mem to H1 H6.

Subgoal 4:

Variables: L S Q T F A
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H5 : {L, [F] |- sub S Q}
H6 : member F L
H7 : name A
H8 : F = sub A A \/ (exists T, F = sub A T) \/ F =
pi U\pi V\sub A U => sub U V => sub A V
============================
{L |- sub S T}

transitivity < case H8.

Subgoal 4.1:

Variables: L S Q T A
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H5 : {L, [sub A A] |- sub S Q}
H6 : member (sub A A) L
H7 : name A
============================
{L |- sub S T}

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

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

transitivity < case H5.

Subgoal 4.1:

Variables: L Q T
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H6 : member (sub Q Q) L
H7 : name Q
============================
{L |- sub Q T}

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

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

transitivity < search.

Subgoal 4.2:

Variables: L S Q T A T1
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H5 : {L, [sub A T1] |- sub S Q}
H6 : member (sub A T1) L
H7 : name A
============================
{L |- sub S T}

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

transitivity < case H5.

Subgoal 4.2:

Variables: L S Q T
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H6 : member (sub S Q) L
H7 : name S
============================
{L |- sub S T}

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

transitivity < apply ctx_sync to H1 H6.

Subgoal 4.2:

Variables: L S Q T
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H6 : member (sub S Q) L
H7 : name S
H9 : member (pi U\pi V\sub S U => sub U V => sub S V) L
============================
{L |- sub S T}

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

transitivity < search.

Subgoal 4.3:

Variables: L S Q T A
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H5 : {L, [pi U\pi V\sub A U => sub U V => sub A V] |- sub S Q}
H6 : member (pi U\pi V\sub A U => sub U V => sub A V) L
H7 : name A
============================
{L |- sub S T}

transitivity < case H5.

Subgoal 4.3:

Variables: L S Q T U
IH : forall L S Q T, ctx L -> tp Q * -> {L |- sub S Q} -> {L |- sub Q T} ->
{L |- sub S T}
H1 : ctx L
H2 : tp Q @
H4 : {L |- sub Q T}
H6 : member (pi U\pi V\sub S U => sub U V => sub S V) L
H7 : name S
H9 : {L |- sub S U}
H10 : {L |- sub U Q}
============================
{L |- sub S T}

transitivity < search.
Proof completed.

Abella <