Welcome to Abella 2.0.5-dev.
Abella < Specification "fsub".
Reading 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 <