Welcome to Abella 2.0.5-dev.
Abella < Specification "fcurry".
Reading specification "fcurry".

Abella < Close ty, tm.

Abella < Theorem member_prune : 
forall L E, nabla x, member (E x) L -> (exists F, E = x\F).


============================
 forall L E, nabla x, member (E x) L -> (exists F, E = x\F)

member_prune < induction on 1.

IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F)
============================
 forall L E, nabla x, member (E x) L @ -> (exists F, E = x\F)

member_prune < intros.

Variables: L E
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F)
H1 : member (E n1) L @
============================
 exists F, E = x\F

member_prune < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F)
============================
 exists F, z1\L2 = x\F

Subgoal 2 is:
 exists F, E = x\F

member_prune < search.
Subgoal 2:

Variables: E L3 L2
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F)
H2 : member (E n1) L3 *
============================
 exists F, E = x\F

member_prune < apply IH to H2.
Subgoal 2:

Variables: L3 L2 F
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F)
H2 : member F L3 *
============================
 exists F1, z1\F = x\F1

member_prune < search.
Proof completed.
Abella < Define ctx : olist -> prop by 
ctx nil;
nabla x, ctx (of x T :: L) := ctx L.

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

Abella < Theorem of_name : 
forall L E, ctx L -> member E L -> (exists X T, E = of X T /\ name X).


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

of_name < induction on 1.

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

of_name < intros.

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

of_name < case H1.
Subgoal 1:

Variables: E
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H2 : member E nil
============================
 exists X T, E = of X T /\ name X

Subgoal 2 is:
 exists X T, E n1 = of X T /\ name X

of_name < case H2.
Subgoal 2:

Variables: E L1 T
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H2 : member (E n1) (of n1 T :: L1)
H3 : ctx L1 *
============================
 exists X T, E n1 = of X T /\ name X

of_name < case H2.
Subgoal 2.1:

Variables: L1 T
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H3 : ctx L1 *
============================
 exists X T1, of n1 T = of X T1 /\ name X

Subgoal 2.2 is:
 exists X T, E n1 = of X T /\ name X

of_name < search.
Subgoal 2.2:

Variables: E L1 T
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H3 : ctx L1 *
H4 : member (E n1) L1
============================
 exists X T, E n1 = of X T /\ name X

of_name < apply member_prune to H4.
Subgoal 2.2:

Variables: L1 T F
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H3 : ctx L1 *
H4 : member F L1
============================
 exists X T, F = of X T /\ name X

of_name < apply IH to H3 H4.
Subgoal 2.2:

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

of_name < search.
Proof completed.
Abella < Theorem ctx_uniq : 
forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 =
T2.


============================
 forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 =
 T2

ctx_uniq < induction on 1.

IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
============================
 forall L E T1 T2, ctx L @ -> member (of E T1) L -> member (of E T2) L ->
   T1 =
 T2

ctx_uniq < intros.

Variables: L E T1 T2
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx L @
H2 : member (of E T1) L
H3 : member (of E T2) L
============================
 T1 = T2

ctx_uniq < case H1.
Subgoal 1:

Variables: E T1 T2
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H2 : member (of E T1) nil
H3 : member (of E T2) nil
============================
 T1 = T2

Subgoal 2 is:
 T1 = T2

ctx_uniq < case H2.
Subgoal 2:

Variables: E T1 T2 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H2 : member (of (E n1) T1) (of n1 T :: L1)
H3 : member (of (E n1) T2) (of n1 T :: L1)
H4 : ctx L1 *
============================
 T1 = T2

ctx_uniq < case H2.
Subgoal 2.1:

Variables: T2 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H3 : member (of n1 T2) (of n1 T :: L1)
H4 : ctx L1 *
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < case H3.
Subgoal 2.1.1:

Variables: L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : ctx L1 *
============================
 T = T

Subgoal 2.1.2 is:
 T = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < search.
Subgoal 2.1.2:

Variables: T2 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : ctx L1 *
H5 : member (of n1 T2) L1
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < apply member_prune to H5.
Subgoal 2.2:

Variables: E T1 T2 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H3 : member (of (E n1) T2) (of n1 T :: L1)
H4 : ctx L1 *
H5 : member (of (E n1) T1) L1
============================
 T1 = T2

ctx_uniq < case H3.
Subgoal 2.2.1:

Variables: T1 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : ctx L1 *
H5 : member (of n1 T1) L1
============================
 T1 = T

Subgoal 2.2.2 is:
 T1 = T2

ctx_uniq < apply member_prune to H5.
Subgoal 2.2.2:

Variables: E T1 T2 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : ctx L1 *
H5 : member (of (E n1) T1) L1
H6 : member (of (E n1) T2) L1
============================
 T1 = T2

ctx_uniq < apply IH to H4 H5 H6.
Subgoal 2.2.2:

Variables: E T2 L1 T
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : ctx L1 *
H5 : member (of (E n1) T2) L1
H6 : member (of (E n1) T2) L1
============================
 T2 = T2

ctx_uniq < search.
Proof completed.
Abella < Theorem abs_ins_arr : 
forall L R N U T S, ctx L -> {L |- of (abs R) S} ->
  {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}.


============================
 forall L R N U T S, ctx L -> {L |- of (abs R) S} ->
   {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}

abs_ins_arr < induction on 2.

IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
============================
 forall L R N U T S, ctx L -> {L |- of (abs R) S}@ ->
   {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}

abs_ins_arr < intros.

Variables: L R N U T S
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H2 : {L |- of (abs R) S}@
H3 : {L |- ins* S (arr U T)}
H4 : {L |- of N U}
============================
 {L |- of (R N) T}

abs_ins_arr < case H2.
Subgoal 1:

Variables: L R N U T U1 T1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* (arr T1 U1) (arr U T)}
H4 : {L |- of N U}
H5 : {L, of n1 T1 |- of (R n1) U1}*
============================
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H3.
Subgoal 1.1:

Variables: L R N U T
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 U |- of (R n1) T}*
============================
 {L |- of (R N) T}

Subgoal 1.2 is:
 {L |- of (R N) T}

Subgoal 1.3 is:
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr <  inst H5 with n1 = N.
Subgoal 1.1:

Variables: L R N U T
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 U |- of (R n1) T}*
H6 : {L, of N U |- of (R N) T}*
============================
 {L |- of (R N) T}

Subgoal 1.2 is:
 {L |- of (R N) T}

Subgoal 1.3 is:
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < cut H6 with H4.
Subgoal 1.1:

Variables: L R N U T
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 U |- of (R n1) T}*
H6 : {L, of N U |- of (R N) T}*
H7 : {L |- of (R N) T}
============================
 {L |- of (R N) T}

Subgoal 1.2 is:
 {L |- of (R N) T}

Subgoal 1.3 is:
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < search.
Subgoal 1.2:

Variables: L R N U T U1 T1 U2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 T1 |- of (R n1) U1}*
H6 : {L |- ins (arr T1 U1) U2}
H7 : {L |- ins* U2 (arr U T)}
============================
 {L |- of (R N) T}

Subgoal 1.3 is:
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H6.
Subgoal 1.2:

Variables: L R N U T U1 T1 U2 F
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 T1 |- of (R n1) U1}*
H7 : {L |- ins* U2 (arr U T)}
H8 : {L, [F] |- ins (arr T1 U1) U2}
H9 : member F L
============================
 {L |- of (R N) T}

Subgoal 1.3 is:
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < apply of_name to _ H9.
Subgoal 1.2:

Variables: L R N U T U1 T1 U2 X T2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 T1 |- of (R n1) U1}*
H7 : {L |- ins* U2 (arr U T)}
H8 : {L, [of X T2] |- ins (arr T1 U1) U2}
H9 : member (of X T2) L
H10 : name X
============================
 {L |- of (R N) T}

Subgoal 1.3 is:
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H8.
Subgoal 1.3:

Variables: L R N U T U1 T1 F
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 T1 |- of (R n1) U1}*
H6 : {L, [F] |- ins* (arr T1 U1) (arr U T)}
H7 : member F L
============================
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < apply of_name to _ H7.
Subgoal 1.3:

Variables: L R N U T U1 T1 X T2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L, of n1 T1 |- of (R n1) U1}*
H6 : {L, [of X T2] |- ins* (arr T1 U1) (arr U T)}
H7 : member (of X T2) L
H8 : name X
============================
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H6.
Subgoal 2:

Variables: L R N U T T1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* (all T1) (arr U T)}
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H3.
Subgoal 2.1:

Variables: L R N U T T1 U1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H6 : {L |- ins (all T1) U1}
H7 : {L |- ins* U1 (arr U T)}
============================
 {L |- of (R N) T}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H6.
Subgoal 2.1.1:

Variables: L R N U T T1 U2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H7 : {L |- ins* (T1 U2) (arr U T)}
============================
 {L |- of (R N) T}

Subgoal 2.1.2 is:
 {L |- of (R N) T}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr <  inst H5 with n1 = U2.
Subgoal 2.1.1:

Variables: L R N U T T1 U2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H7 : {L |- ins* (T1 U2) (arr U T)}
H8 : {L |- of (abs R) (T1 U2)}*
============================
 {L |- of (R N) T}

Subgoal 2.1.2 is:
 {L |- of (R N) T}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < apply IH to _ H8 H7 H4.
Subgoal 2.1.1:

Variables: L R N U T T1 U2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H7 : {L |- ins* (T1 U2) (arr U T)}
H8 : {L |- of (abs R) (T1 U2)}*
H9 : {L |- of (R N) T}
============================
 {L |- of (R N) T}

Subgoal 2.1.2 is:
 {L |- of (R N) T}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < search.
Subgoal 2.1.2:

Variables: L R N U T T1 U1 F
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H7 : {L |- ins* U1 (arr U T)}
H8 : {L, [F] |- ins (all T1) U1}
H9 : member F L
============================
 {L |- of (R N) T}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < apply of_name to _ H9.
Subgoal 2.1.2:

Variables: L R N U T T1 U1 X T2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H7 : {L |- ins* U1 (arr U T)}
H8 : {L, [of X T2] |- ins (all T1) U1}
H9 : member (of X T2) L
H10 : name X
============================
 {L |- of (R N) T}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H8.
Subgoal 2.2:

Variables: L R N U T T1 F
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H6 : {L, [F] |- ins* (all T1) (arr U T)}
H7 : member F L
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < apply of_name to _ H7.
Subgoal 2.2:

Variables: L R N U T T1 X T2
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H4 : {L |- of N U}
H5 : {L |- of (abs R) (T1 n1)}*
H6 : {L, [of X T2] |- ins* (all T1) (arr U T)}
H7 : member (of X T2) L
H8 : name X
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < case H6.
Subgoal 3:

Variables: L R N U T T1 U1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* (T1 U1) (arr U T)}
H4 : {L |- of N U}
H5 : {L |- of (abs R) (all T1)}*
============================
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < assert {L |- ins* (all T1) (arr U T)}.
Subgoal 3:

Variables: L R N U T T1 U1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* (T1 U1) (arr U T)}
H4 : {L |- of N U}
H5 : {L |- of (abs R) (all T1)}*
H6 : {L |- ins* (all T1) (arr U T)}
============================
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < apply IH to _ H5 H6 H4.
Subgoal 3:

Variables: L R N U T T1 U1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* (T1 U1) (arr U T)}
H4 : {L |- of N U}
H5 : {L |- of (abs R) (all T1)}*
H6 : {L |- ins* (all T1) (arr U T)}
H7 : {L |- of (R N) T}
============================
 {L |- of (R N) T}

Subgoal 4 is:
 {L |- of (R N) T}

abs_ins_arr < search.
Subgoal 4:

Variables: L R N U T S F
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* S (arr U T)}
H4 : {L |- of N U}
H5 : {L, [F] |- of (abs R) S}*
H6 : member F L
============================
 {L |- of (R N) T}

abs_ins_arr < apply of_name to _ H6.
Subgoal 4:

Variables: L R N U T S X T1
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* S (arr U T)}
H4 : {L |- of N U}
H5 : {L, [of X T1] |- of (abs R) S}*
H6 : member (of X T1) L
H7 : name X
============================
 {L |- of (R N) T}

abs_ins_arr < case H5.
Subgoal 4:

Variables: L R N U T S
IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* ->
       {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- ins* S (arr U T)}
H4 : {L |- of N U}
H6 : member (of (abs R) S) L
H7 : name (abs R)
============================
 {L |- of (R N) T}

abs_ins_arr < case H7.
Proof completed.
Abella < Theorem abs_arr : 
forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)} -> {L |- of N U} ->
  {L |- of (R N) T}.


============================
 forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)} -> {L |- of N U} ->
   {L |- of (R N) T}

abs_arr < induction on 2.

IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
============================
 forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}@ -> {L |- of N U} ->
   {L |- of (R N) T}

abs_arr < intros.

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H2 : {L |- of (abs R) (arr U T)}@
H3 : {L |- of N U}
============================
 {L |- of (R N) T}

abs_arr < case H2.
Subgoal 1:

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H4 : {L, of n1 U |- of (R n1) T}*
============================
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr <  inst H4 with n1 = N.
Subgoal 1:

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H4 : {L, of n1 U |- of (R n1) T}*
H5 : {L, of N U |- of (R N) T}*
============================
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < cut H5 with H3.
Subgoal 1:

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H4 : {L, of n1 U |- of (R n1) T}*
H5 : {L, of N U |- of (R N) T}*
H6 : {L |- of (R N) T}
============================
 {L |- of (R N) T}

Subgoal 2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < search.
Subgoal 2:

Variables: L R N U T T1 U1
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H4 : T1 U1 = arr U T
H5 : {L |- of (abs R) (all T1)}*
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < case H4.
Subgoal 2.1:

Variables: L R N U1 T3 T2
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N (T2 U1)}
H5 : {L |- of (abs R) (all (z1\arr (T2 z1) (T3 z1)))}*
============================
 {L |- of (R N) (T3 U1)}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < assert {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))}.
Subgoal 2.1:

Variables: L R N U1 T3 T2
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N (T2 U1)}
H5 : {L |- of (abs R) (all (z1\arr (T2 z1) (T3 z1)))}*
H6 : {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))}
============================
 {L |- of (R N) (T3 U1)}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < apply abs_ins_arr to _ H5 H6 H3.
Subgoal 2.1:

Variables: L R N U1 T3 T2
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N (T2 U1)}
H5 : {L |- of (abs R) (all (z1\arr (T2 z1) (T3 z1)))}*
H6 : {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))}
H7 : {L |- of (R N) (T3 U1)}
============================
 {L |- of (R N) (T3 U1)}

Subgoal 2.2 is:
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < search.
Subgoal 2.2:

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H5 : {L |- of (abs R) (all z1\z1)}*
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < assert {L |- ins* (all z1\z1) (arr U T)}.
Subgoal 2.2:

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H5 : {L |- of (abs R) (all z1\z1)}*
H6 : {L |- ins* (all z1\z1) (arr U T)}
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < apply abs_ins_arr to _ H5 H6 H3.
Subgoal 2.2:

Variables: L R N U T
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H5 : {L |- of (abs R) (all z1\z1)}*
H6 : {L |- ins* (all z1\z1) (arr U T)}
H7 : {L |- of (R N) T}
============================
 {L |- of (R N) T}

Subgoal 3 is:
 {L |- of (R N) T}

abs_arr < search.
Subgoal 3:

Variables: L R N U T F
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H4 : {L, [F] |- of (abs R) (arr U T)}*
H5 : member F L
============================
 {L |- of (R N) T}

abs_arr < apply of_name to _ H5.
Subgoal 3:

Variables: L R N U T X T1
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx L
H3 : {L |- of N U}
H4 : {L, [of X T1] |- of (abs R) (arr U T)}*
H5 : member (of X T1) L
H6 : name X
============================
 {L |- of (R N) T}

abs_arr < case H6.
Subgoal 3:

Variables: L R N U T T1
IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* ->
       {L |- of N U} -> {L |- of (R N) T}
H1 : ctx (L n1)
H3 : {L n1 |- of (N n1) U}
H4 : {L n1, [of n1 T1] |- of (abs (R n1)) (arr U T)}*
H5 : member (of n1 T1) (L n1)
============================
 {L n1 |- of (R n1 (N n1)) T}

abs_arr < case H4.
Proof completed.
Abella < Theorem step_preserves_of : 
forall L M N T, ctx L -> {L |- of M T} -> {step M N} -> {L |- of N T}.


============================
 forall L M N T, ctx L -> {L |- of M T} -> {step M N} -> {L |- of N T}

step_preserves_of < induction on 2.

IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
============================
 forall L M N T, ctx L -> {L |- of M T}@ -> {step M N} -> {L |- of N T}

step_preserves_of < intros.

Variables: L M N T
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H2 : {L |- of M T}@
H3 : {step M N}
============================
 {L |- of N T}

step_preserves_of < case H2.
Subgoal 1:

Variables: L N T U N1 M1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step (app M1 N1) N}
H4 : {L |- of M1 (arr U T)}*
H5 : {L |- of N1 U}*
============================
 {L |- of N T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < case H3.
Subgoal 1.1:

Variables: L T U N1 M1 M'
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L |- of M1 (arr U T)}*
H5 : {L |- of N1 U}*
H6 : {step M1 M'}
============================
 {L |- of (app M' N1) T}

Subgoal 1.2 is:
 {L |- of (app M1 N') T}

Subgoal 1.3 is:
 {L |- of (R N1) T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < apply IH to _ H4 H6.
Subgoal 1.1:

Variables: L T U N1 M1 M'
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L |- of M1 (arr U T)}*
H5 : {L |- of N1 U}*
H6 : {step M1 M'}
H7 : {L |- of M' (arr U T)}
============================
 {L |- of (app M' N1) T}

Subgoal 1.2 is:
 {L |- of (app M1 N') T}

Subgoal 1.3 is:
 {L |- of (R N1) T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < search.
Subgoal 1.2:

Variables: L T U N1 M1 N'
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L |- of M1 (arr U T)}*
H5 : {L |- of N1 U}*
H6 : {step N1 N'}
============================
 {L |- of (app M1 N') T}

Subgoal 1.3 is:
 {L |- of (R N1) T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < apply IH to _ H5 H6.
Subgoal 1.2:

Variables: L T U N1 M1 N'
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L |- of M1 (arr U T)}*
H5 : {L |- of N1 U}*
H6 : {step N1 N'}
H7 : {L |- of N' U}
============================
 {L |- of (app M1 N') T}

Subgoal 1.3 is:
 {L |- of (R N1) T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < search.
Subgoal 1.3:

Variables: L T U N1 R
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L |- of (abs R) (arr U T)}*
H5 : {L |- of N1 U}*
============================
 {L |- of (R N1) T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < apply abs_arr to _ H4 H5.
Subgoal 1.3:

Variables: L T U N1 R
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L |- of (abs R) (arr U T)}*
H5 : {L |- of N1 U}*
H6 : {L |- of (R N1) T}
============================
 {L |- of (R N1) T}

Subgoal 2 is:
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < search.
Subgoal 2:

Variables: L N U R T1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step (abs R) N}
H4 : {L, of n1 T1 |- of (R n1) U}*
============================
 {L |- of N (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < case H3.
Subgoal 2:

Variables: L U R T1 R'
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L, of n1 T1 |- of (R n1) U}*
H5 : {step (R n1) (R' n1)}
============================
 {L |- of (abs R') (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < apply IH to _ H4 H5.
Subgoal 2:

Variables: L U R T1 R'
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H4 : {L, of n1 T1 |- of (R n1) U}*
H5 : {step (R n1) (R' n1)}
H6 : {L, of n1 T1 |- of (R' n1) U}
============================
 {L |- of (abs R') (arr T1 U)}

Subgoal 3 is:
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < search.
Subgoal 3:

Variables: L M N T1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H4 : {L |- of M (T1 n1)}*
============================
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < apply IH to _ H4 H3.
Subgoal 3:

Variables: L M N T1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H4 : {L |- of M (T1 n1)}*
H5 : {L |- of N (T1 n1)}
============================
 {L |- of N (all T1)}

Subgoal 4 is:
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < search.
Subgoal 4:

Variables: L M N T1 U
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H4 : {L |- of M (all T1)}*
============================
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < apply IH to _ H4 H3.
Subgoal 4:

Variables: L M N T1 U
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H4 : {L |- of M (all T1)}*
H5 : {L |- of N (all T1)}
============================
 {L |- of N (T1 U)}

Subgoal 5 is:
 {L |- of N T}

step_preserves_of < search.
Subgoal 5:

Variables: L M N T F
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H4 : {L, [F] |- of M T}*
H5 : member F L
============================
 {L |- of N T}

step_preserves_of < apply of_name to _ H5.
Subgoal 5:

Variables: L M N T X T1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H4 : {L, [of X T1] |- of M T}*
H5 : member (of X T1) L
H6 : name X
============================
 {L |- of N T}

step_preserves_of < case H4.
Subgoal 5:

Variables: L M N T
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H3 : {step M N}
H5 : member (of M T) L
H6 : name M
============================
 {L |- of N T}

step_preserves_of < case H3.
Subgoal 5.1:

Variables: L T M' M1 N1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H5 : member (of (app M1 N1) T) L
H6 : name (app M1 N1)
H7 : {step M1 M'}
============================
 {L |- of (app M' N1) T}

Subgoal 5.2 is:
 {L |- of (app M1 N') T}

Subgoal 5.3 is:
 {L |- of (abs R') T}

Subgoal 5.4 is:
 {L |- of (R N1) T}

step_preserves_of < case H6.
Subgoal 5.2:

Variables: L T N' N1 M1
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H5 : member (of (app M1 N1) T) L
H6 : name (app M1 N1)
H7 : {step N1 N'}
============================
 {L |- of (app M1 N') T}

Subgoal 5.3 is:
 {L |- of (abs R') T}

Subgoal 5.4 is:
 {L |- of (R N1) T}

step_preserves_of < case H6.
Subgoal 5.3:

Variables: L T R' R
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H5 : member (of (abs R) T) L
H6 : name (abs R)
H7 : {step (R n1) (R' n1)}
============================
 {L |- of (abs R') T}

Subgoal 5.4 is:
 {L |- of (R N1) T}

step_preserves_of < case H6.
Subgoal 5.4:

Variables: L T N1 R
IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T}
H1 : ctx L
H5 : member (of (app (abs R) N1) T) L
H6 : name (app (abs R) N1)
============================
 {L |- of (R N1) T}

step_preserves_of < case H6.
Proof completed.
Abella <