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

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

Abella < Define ctxs : olist -> olist -> prop by 
ctxs nil nil;
nabla x, ctxs (term x :: L) (neutral x :: K) := ctxs L K.

Abella < Theorem ctxs_member_term : 
forall L K E, ctxs L K -> member E L ->
  (exists X, E = term X /\ member (neutral X) K /\ name X).


============================
 forall L K E, ctxs L K -> member E L ->
   (exists X, E = term X /\ member (neutral X) K /\ name X)

ctxs_member_term < induction on 1.

IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
============================
 forall L K E, ctxs L K @ -> member E L ->
   (exists X, E = term X /\ member (neutral X) K /\ name X)

ctxs_member_term < intros.

Variables: L K E
IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
H1 : ctxs L K @
H2 : member E L
============================
 exists X, E = term X /\ member (neutral X) K /\ name X

ctxs_member_term < case H1.
Subgoal 1:

Variables: E
IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
H2 : member E nil
============================
 exists X, E = term X /\ member (neutral X) nil /\ name X

Subgoal 2 is:
 exists X, E n1 = term X /\ member (neutral X) (neutral n1 :: K1) /\ name X

ctxs_member_term < case H2.
Subgoal 2:

Variables: E K1 L1
IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
H2 : member (E n1) (term n1 :: L1)
H3 : ctxs L1 K1 *
============================
 exists X, E n1 = term X /\ member (neutral X) (neutral n1 :: K1) /\ name X

ctxs_member_term < case H2.
Subgoal 2.1:

Variables: K1 L1
IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
H3 : ctxs L1 K1 *
============================
 exists X, term n1 = term X /\ member (neutral X) (neutral n1 :: K1) /\
   name X

Subgoal 2.2 is:
 exists X, E n1 = term X /\ member (neutral X) (neutral n1 :: K1) /\ name X

ctxs_member_term < search.
Subgoal 2.2:

Variables: E K1 L1
IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
H3 : ctxs L1 K1 *
H4 : member (E n1) L1
============================
 exists X, E n1 = term X /\ member (neutral X) (neutral n1 :: K1) /\ name X

ctxs_member_term < apply IH to H3 H4.
Subgoal 2.2:

Variables: K1 L1 X
IH : forall L K E, ctxs L K * -> member E L ->
       (exists X, E = term X /\ member (neutral X) K /\ name X)
H3 : ctxs L1 K1 *
H4 : member (term (X n1)) L1
H5 : member (neutral (X n1)) K1
H6 : name (X n1)
============================
 exists X1, term (X n1) = term X1 /\
   member (neutral X1) (neutral n1 :: K1) /\ name X1

ctxs_member_term < search.
Proof completed.
Abella < Theorem ctxs_var : 
forall E L K, ctxs L K -> member E K -> (exists X, E = neutral X /\ name X).


============================
 forall E L K, ctxs L K -> member E K -> (exists X, E = neutral X /\ name X)

ctxs_var < induction on 1.

IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
============================
 forall E L K, ctxs L K @ -> member E K ->
   (exists X, E = neutral X /\ name X)

ctxs_var < intros.

Variables: E L K
IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
H1 : ctxs L K @
H2 : member E K
============================
 exists X, E = neutral X /\ name X

ctxs_var < case H1.
Subgoal 1:

Variables: E
IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
H2 : member E nil
============================
 exists X, E = neutral X /\ name X

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

ctxs_var < case H2.
Subgoal 2:

Variables: E K1 L1
IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
H2 : member (E n1) (neutral n1 :: K1)
H3 : ctxs L1 K1 *
============================
 exists X, E n1 = neutral X /\ name X

ctxs_var < case H2.
Subgoal 2.1:

Variables: K1 L1
IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
H3 : ctxs L1 K1 *
============================
 exists X, neutral n1 = neutral X /\ name X

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

ctxs_var < search.
Subgoal 2.2:

Variables: E K1 L1
IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
H3 : ctxs L1 K1 *
H4 : member (E n1) K1
============================
 exists X, E n1 = neutral X /\ name X

ctxs_var < apply IH to H3 H4.
Subgoal 2.2:

Variables: K1 L1 X
IH : forall E L K, ctxs L K * -> member E K ->
       (exists X, E = neutral X /\ name X)
H3 : ctxs L1 K1 *
H4 : member (neutral (X n1)) K1
H5 : name (X n1)
============================
 exists X1, neutral (X n1) = neutral X1 /\ name X1

ctxs_var < search.
Proof completed.
Abella < Theorem total_ext : 
forall T L K, ctxs L K -> {L |- term T} -> {K |- normal T} \/ {non_normal T}.


============================
 forall T L K, ctxs L K -> {L |- term T} -> {K |- normal T} \/ {non_normal T}

total_ext < induction on 2.

IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
============================
 forall T L K, ctxs L K -> {L |- term T}@ -> {K |- normal T} \/
   {non_normal T}

total_ext < intros.

Variables: T L K
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H2 : {L |- term T}@
============================
 {K |- normal T} \/ {non_normal T}

total_ext < case H2.
Subgoal 1:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < apply IH to H1 H3.
Subgoal 1:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H5 : {K |- normal M} \/ {non_normal M}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < apply IH to H1 H4.
Subgoal 1:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H5 : {K |- normal M} \/ {non_normal M}
H6 : {K |- normal N} \/ {non_normal N}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < case H5.
Subgoal 1.1:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H6 : {K |- normal N} \/ {non_normal N}
H7 : {K |- normal M}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < case H6.
Subgoal 1.1.1:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H7 : {K |- normal M}
H8 : {K |- normal N}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < case H7.
Subgoal 1.1.1.1:

Variables: L K N R
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term (abs R)}*
H4 : {L |- term N}*
H8 : {K |- normal N}
H9 : {K, neutral n1 |- normal (R n1)}
============================
 {K |- normal (app (abs R) N)} \/ {non_normal (app (abs R) N)}

Subgoal 1.1.1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.1.3 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Subgoal 1.1.1.2:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H8 : {K |- normal N}
H9 : {K |- neutral M}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.1.3 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Subgoal 1.1.1.3:

Variables: L K N M F
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H8 : {K |- normal N}
H9 : {K, [F] |- normal M}
H10 : member F K
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < apply ctxs_var to H1 H10.
Subgoal 1.1.1.3:

Variables: L K N M X
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H8 : {K |- normal N}
H9 : {K, [neutral X] |- normal M}
H10 : member (neutral X) K
H11 : name X
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < case H9.
Subgoal 1.1.2:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H7 : {K |- normal M}
H8 : {non_normal N}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 1.2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Subgoal 1.2:

Variables: L K N M
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H6 : {K |- normal N} \/ {non_normal N}
H7 : {non_normal M}
============================
 {K |- normal (app M N)} \/ {non_normal (app M N)}

Subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Subgoal 2:

Variables: L K R
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L, term n1 |- term (R n1)}*
============================
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < apply IH to _ H3.
Subgoal 2:

Variables: L K R
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L, term n1 |- term (R n1)}*
H4 : {K, neutral n1 |- normal (R n1)} \/ {non_normal (R n1)}
============================
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < case H4.
Subgoal 2.1:

Variables: L K R
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L, term n1 |- term (R n1)}*
H5 : {K, neutral n1 |- normal (R n1)}
============================
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 2.2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Subgoal 2.2:

Variables: L K R
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L, term n1 |- term (R n1)}*
H5 : {non_normal (R n1)}
============================
 {K |- normal (abs R)} \/ {non_normal (abs R)}

Subgoal 3 is:
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Subgoal 3:

Variables: T L K F
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L, [F] |- term T}*
H4 : member F L
============================
 {K |- normal T} \/ {non_normal T}

total_ext < apply ctxs_member_term to H1 H4.
Subgoal 3:

Variables: T L K X
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H3 : {L, [term X] |- term T}*
H4 : member (term X) L
H5 : member (neutral X) K
H6 : name X
============================
 {K |- normal T} \/ {non_normal T}

total_ext < case H3.
Subgoal 3:

Variables: T L K
IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
       {non_normal T}
H1 : ctxs L K
H4 : member (term T) L
H5 : member (neutral T) K
H6 : name T
============================
 {K |- normal T} \/ {non_normal T}

total_ext < search.
Proof completed.
Abella < Theorem total : 
forall T, {term T} -> {normal T} \/ {non_normal T}.


============================
 forall T, {term T} -> {normal T} \/ {non_normal T}

total < intros.

Variables: T
H1 : {term T}
============================
 {normal T} \/ {non_normal T}

total < apply total_ext to _ H1.

Variables: T
H1 : {term T}
H2 : {normal T} \/ {non_normal T}
============================
 {normal T} \/ {non_normal T}

total < search.
Proof completed.
Abella < Theorem neutral_abs_absurd : 
forall L K R, ctxs L K -> {K |- neutral (abs R)} -> false.


============================
 forall L K R, ctxs L K -> {K |- neutral (abs R)} -> false

neutral_abs_absurd < intros.

Variables: L K R
H1 : ctxs L K
H2 : {K |- neutral (abs R)}
============================
 false

neutral_abs_absurd < case H2.

Variables: L K R F
H1 : ctxs L K
H3 : {K, [F] |- neutral (abs R)}
H4 : member F K
============================
 false

neutral_abs_absurd < apply ctxs_var to H1 H4.

Variables: L K R X
H1 : ctxs L K
H3 : {K, [neutral X] |- neutral (abs R)}
H4 : member (neutral X) K
H5 : name X
============================
 false

neutral_abs_absurd < case H3.

Variables: L K R
H1 : ctxs L K
H4 : member (neutral (abs R)) K
H5 : name (abs R)
============================
 false

neutral_abs_absurd < case H5.
Proof completed.
Abella < Theorem disjoint_ext : 
forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T} -> false.


============================
 forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T} -> false

disjoint_ext < induction on 3.

IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
============================
 forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}@ -> false

disjoint_ext < intros.

Variables: L K T
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H2 : {K |- normal T}
H3 : {non_normal T}@
============================
 false

disjoint_ext < case H2.
Subgoal 1:

Variables: L K R
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal (abs R)}@
H4 : {K, neutral n1 |- normal (R n1)}
============================
 false

Subgoal 2 is:
 false

Subgoal 3 is:
 false

disjoint_ext < case H3.
Subgoal 1:

Variables: L K R
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H4 : {K, neutral n1 |- normal (R n1)}
H5 : {non_normal (R n1)}*
============================
 false

Subgoal 2 is:
 false

Subgoal 3 is:
 false

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

Variables: L K T
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal T}@
H4 : {K |- neutral T}
============================
 false

Subgoal 3 is:
 false

disjoint_ext < case H4.
Subgoal 2.1:

Variables: L K N M
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal (app M N)}@
H5 : {K |- neutral M}
H6 : {K |- normal N}
============================
 false

Subgoal 2.2 is:
 false

Subgoal 3 is:
 false

disjoint_ext < case H3.
Subgoal 2.1.1:

Variables: L K N R
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H5 : {K |- neutral (abs R)}
H6 : {K |- normal N}
============================
 false

Subgoal 2.1.2 is:
 false

Subgoal 2.1.3 is:
 false

Subgoal 2.2 is:
 false

Subgoal 3 is:
 false

disjoint_ext < apply neutral_abs_absurd to H1 H5.
Subgoal 2.1.2:

Variables: L K N M
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H5 : {K |- neutral M}
H6 : {K |- normal N}
H7 : {non_normal M}*
============================
 false

Subgoal 2.1.3 is:
 false

Subgoal 2.2 is:
 false

Subgoal 3 is:
 false

disjoint_ext < apply IH to H1 _ H7.
Subgoal 2.1.3:

Variables: L K N M
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H5 : {K |- neutral M}
H6 : {K |- normal N}
H7 : {non_normal N}*
============================
 false

Subgoal 2.2 is:
 false

Subgoal 3 is:
 false

disjoint_ext < apply IH to H1 H6 H7.
Subgoal 2.2:

Variables: L K T F
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal T}@
H5 : {K, [F] |- neutral T}
H6 : member F K
============================
 false

Subgoal 3 is:
 false

disjoint_ext < apply ctxs_var to H1 H6.
Subgoal 2.2:

Variables: L K T X
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal T}@
H5 : {K, [neutral X] |- neutral T}
H6 : member (neutral X) K
H7 : name X
============================
 false

Subgoal 3 is:
 false

disjoint_ext < case H5.
Subgoal 2.2:

Variables: L K T
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal T}@
H6 : member (neutral T) K
H7 : name T
============================
 false

Subgoal 3 is:
 false

disjoint_ext < case H7.
Subgoal 2.2:

Variables: L K
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs (L n1) (K n1)
H3 : {non_normal n1}@
H6 : member (neutral n1) (K n1)
============================
 false

Subgoal 3 is:
 false

disjoint_ext < case H3.
Subgoal 3:

Variables: L K T F
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal T}@
H4 : {K, [F] |- normal T}
H5 : member F K
============================
 false

disjoint_ext < apply ctxs_var to H1 H5.
Subgoal 3:

Variables: L K T X
IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
H1 : ctxs L K
H3 : {non_normal T}@
H4 : {K, [neutral X] |- normal T}
H5 : member (neutral X) K
H6 : name X
============================
 false

disjoint_ext < case H4.
Proof completed.
Abella < Theorem disjoint : 
forall T, {normal T} -> {non_normal T} -> false.


============================
 forall T, {normal T} -> {non_normal T} -> false

disjoint < intros.

Variables: T
H1 : {normal T}
H2 : {non_normal T}
============================
 false

disjoint < apply disjoint_ext to _ H1 H2.
Proof completed.
Abella <