Welcome to Abella 2.0.4-dev
Abella < Specification "cr".
Reading specification "cr"

Abella < Define ctxs : olist -> olist -> olist -> prop by 
ctxs nil nil nil;
nabla x, ctxs (trm x :: L) (pr1 x x :: K) (cd1 x x :: notabs x :: J) := ctxs L K J.

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

Abella < Theorem trm_worlds : 
forall L K J E, ctxs L K J -> member E L ->
  (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
       member (cd1 A A) J /\ member (notabs A) J).


============================
 forall L K J E, ctxs L K J -> member E L ->
   (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
        member (cd1 A A) J /\ member (notabs A) J)

trm_worlds < induction on 2.

IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
============================
 forall L K J E, ctxs L K J -> member E L @ ->
   (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
        member (cd1 A A) J /\ member (notabs A) J)

trm_worlds < intros.

Variables: L K J E
IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
H1 : ctxs L K J
H2 : member E L @
============================
 exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
   member (notabs A) J

trm_worlds < case H2.
Subgoal 1:

Variables: K J E L1
IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
H1 : ctxs (E :: L1) K J
============================
 exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
   member (notabs A) J

Subgoal 2 is:
 exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
   member (notabs A) J

trm_worlds < case H1.
Subgoal 1:

Variables: J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
H3 : ctxs L2 K1 J1
============================
 exists A, trm n1 = trm A /\ name A /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
   member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1) /\
   member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)

Subgoal 2 is:
 exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
   member (notabs A) J

trm_worlds < search.
Subgoal 2:

Variables: K J E L1 B
IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
H1 : ctxs (B :: L1) K J
H3 : member E L1 *
============================
 exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
   member (notabs A) J

trm_worlds < case H1.
Subgoal 2:

Variables: E J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
H3 : member (E n1) L2 *
H4 : ctxs L2 K1 J1
============================
 exists A, E n1 = trm A /\ name A /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
   member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1) /\
   member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)

trm_worlds < apply IH to H4 H3.
Subgoal 2:

Variables: J1 K1 L2 A
IH : forall L K J E, ctxs L K J -> member E L * ->
       (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\
            member (cd1 A A) J /\ member (notabs A) J)
H3 : member (trm (A n1)) L2 *
H4 : ctxs L2 K1 J1
H5 : name (A n1)
H6 : member (pr1 (A n1) (A n1)) K1
H7 : member (cd1 (A n1) (A n1)) J1
H8 : member (notabs (A n1)) J1
============================
 exists A1, trm (A n1) = trm A1 /\ name A1 /\
   member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\
   member (cd1 A1 A1) (cd1 n1 n1 :: notabs n1 :: J1) /\
   member (notabs A1) (cd1 n1 n1 :: notabs n1 :: J1)

trm_worlds < search.
Proof completed.
Abella < Theorem pr1_worlds : 
forall L K J E, ctxs L K J -> member E K ->
  (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
       member (cd1 A B) J /\ member (notabs A) J).


============================
 forall L K J E, ctxs L K J -> member E K ->
   (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
        member (cd1 A B) J /\ member (notabs A) J)

pr1_worlds < induction on 2.

IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
============================
 forall L K J E, ctxs L K J -> member E K @ ->
   (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
        member (cd1 A B) J /\ member (notabs A) J)

pr1_worlds < intros.

Variables: L K J E
IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
H1 : ctxs L K J
H2 : member E K @
============================
 exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
   member (cd1 A B) J /\ member (notabs A) J

pr1_worlds < case H2.
Subgoal 1:

Variables: L J E L1
IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
H1 : ctxs L (E :: L1) J
============================
 exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
   member (cd1 A B) J /\ member (notabs A) J

Subgoal 2 is:
 exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
   member (cd1 A B) J /\ member (notabs A) J

pr1_worlds < case H1.
Subgoal 1:

Variables: J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
H3 : ctxs L2 K1 J1
============================
 exists A B, pr1 n1 n1 = pr1 A B /\ name A /\ A = B /\
   member (trm A) (trm n1 :: L2) /\
   member (cd1 A B) (cd1 n1 n1 :: notabs n1 :: J1) /\
   member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)

Subgoal 2 is:
 exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
   member (cd1 A B) J /\ member (notabs A) J

pr1_worlds < search.
Subgoal 2:

Variables: L J E L1 B
IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
H1 : ctxs L (B :: L1) J
H3 : member E L1 *
============================
 exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
   member (cd1 A B) J /\ member (notabs A) J

pr1_worlds < case H1.
Subgoal 2:

Variables: E J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
H3 : member (E n1) K1 *
H4 : ctxs L2 K1 J1
============================
 exists A B, E n1 = pr1 A B /\ name A /\ A = B /\
   member (trm A) (trm n1 :: L2) /\
   member (cd1 A B) (cd1 n1 n1 :: notabs n1 :: J1) /\
   member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)

pr1_worlds < apply IH to H4 H3.
Subgoal 2:

Variables: J1 K1 L2 B1
IH : forall L K J E, ctxs L K J -> member E K * ->
       (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (cd1 A B) J /\ member (notabs A) J)
H3 : member (pr1 (B1 n1) (B1 n1)) K1 *
H4 : ctxs L2 K1 J1
H5 : name (B1 n1)
H6 : member (trm (B1 n1)) L2
H7 : member (cd1 (B1 n1) (B1 n1)) J1
H8 : member (notabs (B1 n1)) J1
============================
 exists A B, pr1 (B1 n1) (B1 n1) = pr1 A B /\ name A /\ A = B /\
   member (trm A) (trm n1 :: L2) /\
   member (cd1 A B) (cd1 n1 n1 :: notabs n1 :: J1) /\
   member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)

pr1_worlds < search.
Proof completed.
Abella < Theorem cd_worlds : 
forall L K J E, ctxs L K J -> member E J ->
  (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
       member (pr1 A A) K /\ member (notabs A) J) \/
  (exists A, E = notabs A /\ name A /\ member (trm A) L /\
       member (pr1 A A) K /\ member (cd1 A A) J).


============================
 forall L K J E, ctxs L K J -> member E J ->
   (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
        member (pr1 A A) K /\ member (notabs A) J) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) J)

cd_worlds < induction on 2.

IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 forall L K J E, ctxs L K J -> member E J @ ->
   (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
        member (pr1 A A) K /\ member (notabs A) J) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) J)

cd_worlds < intros.

Variables: L K J E
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H1 : ctxs L K J
H2 : member E J @
============================
 (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
      member (pr1 A A) K /\ member (notabs A) J) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) J)

cd_worlds < case H2.
Subgoal 1:

Variables: L K E L1
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H1 : ctxs L K (E :: L1)
============================
 (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
      member (pr1 A A) K /\ member (notabs A) (E :: L1)) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) (E :: L1))

Subgoal 2 is:
 (exists A B1, E = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) L /\
      member (pr1 A A) K /\ member (notabs A) (B :: L1)) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) (B :: L1))

cd_worlds < case H1.
Subgoal 1:

Variables: J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H3 : ctxs L2 K1 J1
============================
 (exists A B, cd1 n1 n1 = cd1 A B /\ name A /\ A = B /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, cd1 n1 n1 = notabs A /\ name A /\
        member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

Subgoal 2 is:
 (exists A B1, E = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) L /\
      member (pr1 A A) K /\ member (notabs A) (B :: L1)) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) (B :: L1))

cd_worlds < search.
Subgoal 2:

Variables: L K E L1 B
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H1 : ctxs L K (B :: L1)
H3 : member E L1 *
============================
 (exists A B1, E = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) L /\
      member (pr1 A A) K /\ member (notabs A) (B :: L1)) \/
   (exists A, E = notabs A /\ name A /\ member (trm A) L /\
        member (pr1 A A) K /\ member (cd1 A A) (B :: L1))

cd_worlds < case H1.
Subgoal 2:

Variables: E J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H3 : member (E n1) (notabs n1 :: J1) *
H4 : ctxs L2 K1 J1
============================
 (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < case H3.
Subgoal 2.1:

Variables: J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H4 : ctxs L2 K1 J1
============================
 (exists A B1, notabs n1 = cd1 A B1 /\ name A /\ A = B1 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, notabs n1 = notabs A /\ name A /\
        member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

Subgoal 2.2 is:
 (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < right.
Subgoal 2.1:

Variables: J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H4 : ctxs L2 K1 J1
============================
 exists A, notabs n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\
   member (pr1 A A) (pr1 n1 n1 :: K1) /\
   member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)

Subgoal 2.2 is:
 (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < search.
Subgoal 2.2:

Variables: E J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H4 : ctxs L2 K1 J1
H5 : member (E n1) J1 *
============================
 (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < apply IH to H4 H5.
Subgoal 2.2:

Variables: E J1 K1 L2
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H4 : ctxs L2 K1 J1
H5 : member (E n1) J1 *
H6 : (exists A B, E n1 = cd1 A B /\ name A /\ A = B /\ member (trm A) L2 /\
          member (pr1 A A) K1 /\ member (notabs A) J1) \/
       (exists A, E n1 = notabs A /\ name A /\ member (trm A) L2 /\
            member (pr1 A A) K1 /\ member (cd1 A A) J1)
============================
 (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < case H6.
Subgoal 2.2.1:

Variables: J1 K1 L2 B1
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H4 : ctxs L2 K1 J1
H5 : member (cd1 (B1 n1) (B1 n1)) J1 *
H7 : name (B1 n1)
H8 : member (trm (B1 n1)) L2
H9 : member (pr1 (B1 n1) (B1 n1)) K1
H10 : member (notabs (B1 n1)) J1
============================
 (exists A B2, cd1 (B1 n1) (B1 n1) = cd1 A B2 /\ name A /\ A = B2 /\
      member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\
      member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A, cd1 (B1 n1) (B1 n1) = notabs A /\ name A /\
        member (trm A) (trm n1 :: L2) /\
        member (pr1 A A) (pr1 n1 n1 :: K1) /\
        member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1))

Subgoal 2.2.2 is:
 (exists A1 B1, notabs (A n1) = cd1 A1 B1 /\ name A1 /\ A1 = B1 /\
      member (trm A1) (trm n1 :: L2) /\
      member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\
      member (notabs A1) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A1, notabs (A n1) = notabs A1 /\ name A1 /\
        member (trm A1) (trm n1 :: L2) /\
        member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\
        member (cd1 A1 A1) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < search.
Subgoal 2.2.2:

Variables: J1 K1 L2 A
IH : forall L K J E, ctxs L K J -> member E J * ->
       (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
            member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, E = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
H4 : ctxs L2 K1 J1
H5 : member (notabs (A n1)) J1 *
H7 : name (A n1)
H8 : member (trm (A n1)) L2
H9 : member (pr1 (A n1) (A n1)) K1
H10 : member (cd1 (A n1) (A n1)) J1
============================
 (exists A1 B1, notabs (A n1) = cd1 A1 B1 /\ name A1 /\ A1 = B1 /\
      member (trm A1) (trm n1 :: L2) /\
      member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\
      member (notabs A1) (cd1 n1 n1 :: notabs n1 :: J1)) \/
   (exists A1, notabs (A n1) = notabs A1 /\ name A1 /\
        member (trm A1) (trm n1 :: L2) /\
        member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\
        member (cd1 A1 A1) (cd1 n1 n1 :: notabs n1 :: J1))

cd_worlds < search.
Proof completed.
Abella < Theorem notabs_abs_absurd : 
forall A L K J, ctxs L K J -> {J |- notabs (abs A)} -> false.


============================
 forall A L K J, ctxs L K J -> {J |- notabs (abs A)} -> false

notabs_abs_absurd < intros.

Variables: A L K J
H1 : ctxs L K J
H2 : {J |- notabs (abs A)}
============================
 false

notabs_abs_absurd < case H2.

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

notabs_abs_absurd < apply cd_worlds to H1 H4.

Variables: A L K J F
H1 : ctxs L K J
H3 : {J, [F] |- notabs (abs A)}
H4 : member F J
H5 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 false

notabs_abs_absurd < case H5.
Subgoal 1:

Variables: A L K J B
H1 : ctxs L K J
H3 : {J, [cd1 B B] |- notabs (abs A)}
H4 : member (cd1 B B) J
H6 : name B
H7 : member (trm B) L
H8 : member (pr1 B B) K
H9 : member (notabs B) J
============================
 false

Subgoal 2 is:
 false

notabs_abs_absurd < case H3.
Subgoal 2:

Variables: A L K J A1
H1 : ctxs L K J
H3 : {J, [notabs A1] |- notabs (abs A)}
H4 : member (notabs A1) J
H6 : name A1
H7 : member (trm A1) L
H8 : member (pr1 A1 A1) K
H9 : member (cd1 A1 A1) J
============================
 false

notabs_abs_absurd < case H3.
Subgoal 2:

Variables: A L K J
H1 : ctxs L K J
H4 : member (notabs (abs A)) J
H6 : name (abs A)
H7 : member (trm (abs A)) L
H8 : member (pr1 (abs A) (abs A)) K
H9 : member (cd1 (abs A) (abs A)) J
============================
 false

notabs_abs_absurd < case H6.
Proof completed.
Abella < Theorem cd1_trm : 
forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}.


============================
 forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}

cd1_trm < induction on 2.

IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
============================
 forall A B L K J, ctxs L K J -> {J |- cd1 A B}@ -> {L |- trm A}

cd1_trm < intros.

Variables: A B L K J
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H2 : {J |- cd1 A B}@
============================
 {L |- trm A}

cd1_trm < case H2.
Subgoal 1:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J |- notabs T1}*
H4 : {J |- cd1 T1 T2}*
H5 : {J |- cd1 S1 S2}*
============================
 {L |- trm (app T1 S1)}

Subgoal 2 is:
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < apply IH to H1 H4.
Subgoal 1:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J |- notabs T1}*
H4 : {J |- cd1 T1 T2}*
H5 : {J |- cd1 S1 S2}*
H6 : {L |- trm T1}
============================
 {L |- trm (app T1 S1)}

Subgoal 2 is:
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < apply IH to H1 H5.
Subgoal 1:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J |- notabs T1}*
H4 : {J |- cd1 T1 T2}*
H5 : {J |- cd1 S1 S2}*
H6 : {L |- trm T1}
H7 : {L |- trm S1}
============================
 {L |- trm (app T1 S1)}

Subgoal 2 is:
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < search.
Subgoal 2:

Variables: L K J S2 S1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
============================
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < apply IH to _ H3.
Subgoal 2:

Variables: L K J S2 S1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H4 : {L, trm n1 |- trm (S1 n1)}
============================
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < search.
Subgoal 3:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J |- cd1 (abs T1) (abs T2)}*
H4 : {J |- cd1 S1 S2}*
============================
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < apply IH to H1 H3.
Subgoal 3:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J |- cd1 (abs T1) (abs T2)}*
H4 : {J |- cd1 S1 S2}*
H5 : {L |- trm (abs T1)}
============================
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < apply IH to H1 H4.
Subgoal 3:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J |- cd1 (abs T1) (abs T2)}*
H4 : {J |- cd1 S1 S2}*
H5 : {L |- trm (abs T1)}
H6 : {L |- trm S1}
============================
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

cd1_trm < search.
Subgoal 4:

Variables: A B L K J F
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J, [F] |- cd1 A B}*
H4 : member F J
============================
 {L |- trm A}

cd1_trm < apply cd_worlds to H1 H4.
Subgoal 4:

Variables: A B L K J F
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J, [F] |- cd1 A B}*
H4 : member F J
H5 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 {L |- trm A}

cd1_trm < case H5.
Subgoal 4.1:

Variables: A B L K J B1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J, [cd1 B1 B1] |- cd1 A B}*
H4 : member (cd1 B1 B1) J
H6 : name B1
H7 : member (trm B1) L
H8 : member (pr1 B1 B1) K
H9 : member (notabs B1) J
============================
 {L |- trm A}

Subgoal 4.2 is:
 {L |- trm A}

cd1_trm < case H3.
Subgoal 4.1:

Variables: B L K J
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H4 : member (cd1 B B) J
H6 : name B
H7 : member (trm B) L
H8 : member (pr1 B B) K
H9 : member (notabs B) J
============================
 {L |- trm B}

Subgoal 4.2 is:
 {L |- trm A}

cd1_trm < search.
Subgoal 4.2:

Variables: A B L K J A1
IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {J, [notabs A1] |- cd1 A B}*
H4 : member (notabs A1) J
H6 : name A1
H7 : member (trm A1) L
H8 : member (pr1 A1 A1) K
H9 : member (cd1 A1 A1) J
============================
 {L |- trm A}

cd1_trm < case H3.
Proof completed.
Abella < Theorem pr1_trm : 
forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> {L |- trm A}.


============================
 forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> {L |- trm A}

pr1_trm < induction on 2.

IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
============================
 forall A B L K J, ctxs L K J -> {K |- pr1 A B}@ -> {L |- trm A}

pr1_trm < intros.

Variables: A B L K J
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H2 : {K |- pr1 A B}@
============================
 {L |- trm A}

pr1_trm < case H2.
Subgoal 1:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K |- pr1 T1 T2}*
H4 : {K |- pr1 S1 S2}*
============================
 {L |- trm (app T1 S1)}

Subgoal 2 is:
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < apply IH to H1 H3.
Subgoal 1:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K |- pr1 T1 T2}*
H4 : {K |- pr1 S1 S2}*
H5 : {L |- trm T1}
============================
 {L |- trm (app T1 S1)}

Subgoal 2 is:
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < apply IH to H1 H4.
Subgoal 1:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K |- pr1 T1 T2}*
H4 : {K |- pr1 S1 S2}*
H5 : {L |- trm T1}
H6 : {L |- trm S1}
============================
 {L |- trm (app T1 S1)}

Subgoal 2 is:
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < search.
Subgoal 2:

Variables: L K J S2 S1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
============================
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < apply IH to _ H3.
Subgoal 2:

Variables: L K J S2 S1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
H4 : {L, trm n1 |- trm (S1 n1)}
============================
 {L |- trm (abs S1)}

Subgoal 3 is:
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < search.
Subgoal 3:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K |- pr1 (abs T1) (abs T2)}*
H4 : {K |- pr1 S1 S2}*
============================
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < apply IH to H1 H3.
Subgoal 3:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K |- pr1 (abs T1) (abs T2)}*
H4 : {K |- pr1 S1 S2}*
H5 : {L |- trm (abs T1)}
============================
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < apply IH to H1 H4.
Subgoal 3:

Variables: L K J S2 S1 T2 T1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K |- pr1 (abs T1) (abs T2)}*
H4 : {K |- pr1 S1 S2}*
H5 : {L |- trm (abs T1)}
H6 : {L |- trm S1}
============================
 {L |- trm (app (abs T1) S1)}

Subgoal 4 is:
 {L |- trm A}

pr1_trm < search.
Subgoal 4:

Variables: A B L K J F
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K, [F] |- pr1 A B}*
H4 : member F K
============================
 {L |- trm A}

pr1_trm < apply pr1_worlds to H1 H4.
Subgoal 4:

Variables: A B L K J B1
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H3 : {K, [pr1 B1 B1] |- pr1 A B}*
H4 : member (pr1 B1 B1) K
H5 : name B1
H6 : member (trm B1) L
H7 : member (cd1 B1 B1) J
H8 : member (notabs B1) J
============================
 {L |- trm A}

pr1_trm < case H3.
Subgoal 4:

Variables: B L K J
IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A}
H1 : ctxs L K J
H4 : member (pr1 B B) K
H5 : name B
H6 : member (trm B) L
H7 : member (cd1 B B) J
H8 : member (notabs B) J
============================
 {L |- trm B}

pr1_trm < search.
Proof completed.
Abella < Theorem pre_cd1_pr1 : 
forall A B L K J, ctxs L K J -> {L |- trm A} -> {J |- cd1 A B} ->
  {K |- pr1 A B}.


============================
 forall A B L K J, ctxs L K J -> {L |- trm A} -> {J |- cd1 A B} ->
   {K |- pr1 A B}

pre_cd1_pr1 < induction on 2.

IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
============================
 forall A B L K J, ctxs L K J -> {L |- trm A}@ -> {J |- cd1 A B} ->
   {K |- pr1 A B}

pre_cd1_pr1 < intros.

Variables: A B L K J
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm A}@
H3 : {J |- cd1 A B}
============================
 {K |- pr1 A B}

pre_cd1_pr1 < case H2 (keep).
Subgoal 1:

Variables: B L K J N M
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H3 : {J |- cd1 (app M N) B}
H4 : {L |- trm M}*
H5 : {L |- trm N}*
============================
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H3.
Subgoal 1.1:

Variables: L K J N M S2 T2
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J |- notabs M}
H7 : {J |- cd1 M T2}
H8 : {J |- cd1 N S2}
============================
 {K |- pr1 (app M N) (app T2 S2)}

Subgoal 1.2 is:
 {K |- pr1 (app (abs T1) N) (T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply IH to H1 H4 H7.
Subgoal 1.1:

Variables: L K J N M S2 T2
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J |- notabs M}
H7 : {J |- cd1 M T2}
H8 : {J |- cd1 N S2}
H9 : {K |- pr1 M T2}
============================
 {K |- pr1 (app M N) (app T2 S2)}

Subgoal 1.2 is:
 {K |- pr1 (app (abs T1) N) (T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply IH to H1 H5 H8.
Subgoal 1.1:

Variables: L K J N M S2 T2
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J |- notabs M}
H7 : {J |- cd1 M T2}
H8 : {J |- cd1 N S2}
H9 : {K |- pr1 M T2}
H10 : {K |- pr1 N S2}
============================
 {K |- pr1 (app M N) (app T2 S2)}

Subgoal 1.2 is:
 {K |- pr1 (app (abs T1) N) (T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < search.
Subgoal 1.2:

Variables: L K J N S2 T2 T1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app (abs T1) N)}@
H4 : {L |- trm (abs T1)}*
H5 : {L |- trm N}*
H6 : {J |- cd1 (abs T1) (abs T2)}
H7 : {J |- cd1 N S2}
============================
 {K |- pr1 (app (abs T1) N) (T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply IH to H1 H4 H6.
Subgoal 1.2:

Variables: L K J N S2 T2 T1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app (abs T1) N)}@
H4 : {L |- trm (abs T1)}*
H5 : {L |- trm N}*
H6 : {J |- cd1 (abs T1) (abs T2)}
H7 : {J |- cd1 N S2}
H8 : {K |- pr1 (abs T1) (abs T2)}
============================
 {K |- pr1 (app (abs T1) N) (T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply IH to H1 H5 H7.
Subgoal 1.2:

Variables: L K J N S2 T2 T1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app (abs T1) N)}@
H4 : {L |- trm (abs T1)}*
H5 : {L |- trm N}*
H6 : {J |- cd1 (abs T1) (abs T2)}
H7 : {J |- cd1 N S2}
H8 : {K |- pr1 (abs T1) (abs T2)}
H9 : {K |- pr1 N S2}
============================
 {K |- pr1 (app (abs T1) N) (T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < search.
Subgoal 1.3:

Variables: B L K J N M F
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J, [F] |- cd1 (app M N) B}
H7 : member F J
============================
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply cd_worlds to H1 H7.
Subgoal 1.3:

Variables: B L K J N M F
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J, [F] |- cd1 (app M N) B}
H7 : member F J
H8 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H8.
Subgoal 1.3.1:

Variables: B L K J N M B1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J, [cd1 B1 B1] |- cd1 (app M N) B}
H7 : member (cd1 B1 B1) J
H9 : name B1
H10 : member (trm B1) L
H11 : member (pr1 B1 B1) K
H12 : member (notabs B1) J
============================
 {K |- pr1 (app M N) B}

Subgoal 1.3.2 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H9.
Subgoal 1.3.1:

Variables: B L K J N M
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm (app (M n1) (N n1))}@
H4 : {L n1 |- trm (M n1)}*
H5 : {L n1 |- trm (N n1)}*
H6 : {J n1, [cd1 n1 n1] |- cd1 (app (M n1) (N n1)) (B n1)}
H7 : member (cd1 n1 n1) (J n1)
H10 : member (trm n1) (L n1)
H11 : member (pr1 n1 n1) (K n1)
H12 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 (app (M n1) (N n1)) (B n1)}

Subgoal 1.3.2 is:
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H6.
Subgoal 1.3.2:

Variables: B L K J N M A1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (app M N)}@
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : {J, [notabs A1] |- cd1 (app M N) B}
H7 : member (notabs A1) J
H9 : name A1
H10 : member (trm A1) L
H11 : member (pr1 A1 A1) K
H12 : member (cd1 A1 A1) J
============================
 {K |- pr1 (app M N) B}

Subgoal 2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H6.
Subgoal 2:

Variables: B L K J R
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H3 : {J |- cd1 (abs R) B}
H4 : {L, trm n1 |- trm (R n1)}*
============================
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H3.
Subgoal 2.1:

Variables: L K J R S2
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H4 : {L, trm n1 |- trm (R n1)}*
H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (S2 n1)}
============================
 {K |- pr1 (abs R) (abs S2)}

Subgoal 2.2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply IH to _ H4 H5.
Subgoal 2.1:

Variables: L K J R S2
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H4 : {L, trm n1 |- trm (R n1)}*
H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (S2 n1)}
H6 : {K, pr1 n1 n1 |- pr1 (R n1) (S2 n1)}
============================
 {K |- pr1 (abs R) (abs S2)}

Subgoal 2.2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < search.
Subgoal 2.2:

Variables: B L K J R F
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H4 : {L, trm n1 |- trm (R n1)}*
H5 : {J, [F] |- cd1 (abs R) B}
H6 : member F J
============================
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < apply cd_worlds to H1 H6.
Subgoal 2.2:

Variables: B L K J R F
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H4 : {L, trm n1 |- trm (R n1)}*
H5 : {J, [F] |- cd1 (abs R) B}
H6 : member F J
H7 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H7.
Subgoal 2.2.1:

Variables: B L K J R B1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H4 : {L, trm n1 |- trm (R n1)}*
H5 : {J, [cd1 B1 B1] |- cd1 (abs R) B}
H6 : member (cd1 B1 B1) J
H8 : name B1
H9 : member (trm B1) L
H10 : member (pr1 B1 B1) K
H11 : member (notabs B1) J
============================
 {K |- pr1 (abs R) B}

Subgoal 2.2.2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H8.
Subgoal 2.2.1:

Variables: B L K J R
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n2) (K n2) (J n2)
H2 : {L n2 |- trm (abs (R n2))}@
H4 : {L n2, trm n1 |- trm (R n2 n1)}*
H5 : {J n2, [cd1 n2 n2] |- cd1 (abs (R n2)) (B n2)}
H6 : member (cd1 n2 n2) (J n2)
H9 : member (trm n2) (L n2)
H10 : member (pr1 n2 n2) (K n2)
H11 : member (notabs n2) (J n2)
============================
 {K n2 |- pr1 (abs (R n2)) (B n2)}

Subgoal 2.2.2 is:
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H5.
Subgoal 2.2.2:

Variables: B L K J R A1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm (abs R)}@
H4 : {L, trm n1 |- trm (R n1)}*
H5 : {J, [notabs A1] |- cd1 (abs R) B}
H6 : member (notabs A1) J
H8 : name A1
H9 : member (trm A1) L
H10 : member (pr1 A1 A1) K
H11 : member (cd1 A1 A1) J
============================
 {K |- pr1 (abs R) B}

Subgoal 3 is:
 {K |- pr1 A B}

pre_cd1_pr1 < case H5.
Subgoal 3:

Variables: A B L K J F
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm A}@
H3 : {J |- cd1 A B}
H4 : {L, [F] |- trm A}*
H5 : member F L
============================
 {K |- pr1 A B}

pre_cd1_pr1 < apply trm_worlds to H1 H5.
Subgoal 3:

Variables: A B L K J A1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm A}@
H3 : {J |- cd1 A B}
H4 : {L, [trm A1] |- trm A}*
H5 : member (trm A1) L
H6 : name A1
H7 : member (pr1 A1 A1) K
H8 : member (cd1 A1 A1) J
H9 : member (notabs A1) J
============================
 {K |- pr1 A B}

pre_cd1_pr1 < case H4.
Subgoal 3:

Variables: A B L K J
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs L K J
H2 : {L |- trm A}@
H3 : {J |- cd1 A B}
H5 : member (trm A) L
H6 : name A
H7 : member (pr1 A A) K
H8 : member (cd1 A A) J
H9 : member (notabs A) J
============================
 {K |- pr1 A B}

pre_cd1_pr1 < case H6.
Subgoal 3:

Variables: B L K J
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm n1}@
H3 : {J n1 |- cd1 n1 (B n1)}
H5 : member (trm n1) (L n1)
H7 : member (pr1 n1 n1) (K n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 n1 (B n1)}

pre_cd1_pr1 < case H3.
Subgoal 3:

Variables: B L K J F1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm n1}@
H5 : member (trm n1) (L n1)
H7 : member (pr1 n1 n1) (K n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
H10 : {J n1, [F1 n1] |- cd1 n1 (B n1)}
H11 : member (F1 n1) (J n1)
============================
 {K n1 |- pr1 n1 (B n1)}

pre_cd1_pr1 < apply cd_worlds to H1 H11.
Subgoal 3:

Variables: B L K J F1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm n1}@
H5 : member (trm n1) (L n1)
H7 : member (pr1 n1 n1) (K n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
H10 : {J n1, [F1 n1] |- cd1 n1 (B n1)}
H11 : member (F1 n1) (J n1)
H12 : (exists A B, F1 n1 = cd1 A B /\ name A /\ A = B /\
           member (trm A) (L n1) /\ member (pr1 A A) (K n1) /\
           member (notabs A) (J n1)) \/
        (exists A, F1 n1 = notabs A /\ name A /\ member (trm A) (L n1) /\
             member (pr1 A A) (K n1) /\ member (cd1 A A) (J n1))
============================
 {K n1 |- pr1 n1 (B n1)}

pre_cd1_pr1 < case H12.
Subgoal 3.1:

Variables: B L K J B1
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm n1}@
H5 : member (trm n1) (L n1)
H7 : member (pr1 n1 n1) (K n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
H10 : {J n1, [cd1 (B1 n1) (B1 n1)] |- cd1 n1 (B n1)}
H11 : member (cd1 (B1 n1) (B1 n1)) (J n1)
H13 : name (B1 n1)
H14 : member (trm (B1 n1)) (L n1)
H15 : member (pr1 (B1 n1) (B1 n1)) (K n1)
H16 : member (notabs (B1 n1)) (J n1)
============================
 {K n1 |- pr1 n1 (B n1)}

Subgoal 3.2 is:
 {K n1 |- pr1 n1 (B n1)}

pre_cd1_pr1 < case H10.
Subgoal 3.1:

Variables: L K J
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm n1}@
H5 : member (trm n1) (L n1)
H7 : member (pr1 n1 n1) (K n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
H11 : member (cd1 n1 n1) (J n1)
H13 : name n1
H14 : member (trm n1) (L n1)
H15 : member (pr1 n1 n1) (K n1)
H16 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 n1 n1}

Subgoal 3.2 is:
 {K n1 |- pr1 n1 (B n1)}

pre_cd1_pr1 < search.
Subgoal 3.2:

Variables: B L K J A2
IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} ->
       {K |- pr1 A B}
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {L n1 |- trm n1}@
H5 : member (trm n1) (L n1)
H7 : member (pr1 n1 n1) (K n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
H10 : {J n1, [notabs (A2 n1)] |- cd1 n1 (B n1)}
H11 : member (notabs (A2 n1)) (J n1)
H13 : name (A2 n1)
H14 : member (trm (A2 n1)) (L n1)
H15 : member (pr1 (A2 n1) (A2 n1)) (K n1)
H16 : member (cd1 (A2 n1) (A2 n1)) (J n1)
============================
 {K n1 |- pr1 n1 (B n1)}

pre_cd1_pr1 < case H10.
Proof completed.
Abella < Theorem cd1_pr1 : 
forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}.


============================
 forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}

cd1_pr1 < intros.

Variables: A B L K J
H1 : ctxs L K J
H2 : {J |- cd1 A B}
============================
 {K |- pr1 A B}

cd1_pr1 < apply cd1_trm to H1 H2.

Variables: A B L K J
H1 : ctxs L K J
H2 : {J |- cd1 A B}
H3 : {L |- trm A}
============================
 {K |- pr1 A B}

cd1_pr1 < apply pre_cd1_pr1 to H1 H3 H2.

Variables: A B L K J
H1 : ctxs L K J
H2 : {J |- cd1 A B}
H3 : {L |- trm A}
H4 : {K |- pr1 A B}
============================
 {K |- pr1 A B}

cd1_pr1 < search.
Proof completed.
Abella < Theorem pr1_rfl : 
forall A L K J, ctxs L K J -> {L |- trm A} -> {K |- pr1 A A}.


============================
 forall A L K J, ctxs L K J -> {L |- trm A} -> {K |- pr1 A A}

pr1_rfl < induction on 2.

IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
============================
 forall A L K J, ctxs L K J -> {L |- trm A}@ -> {K |- pr1 A A}

pr1_rfl < intros.

Variables: A L K J
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H2 : {L |- trm A}@
============================
 {K |- pr1 A A}

pr1_rfl < case H2.
Subgoal 1:

Variables: L K J N M
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L |- trm M}*
H4 : {L |- trm N}*
============================
 {K |- pr1 (app M N) (app M N)}

Subgoal 2 is:
 {K |- pr1 (abs R) (abs R)}

Subgoal 3 is:
 {K |- pr1 A A}

pr1_rfl < apply IH to H1 H3.
Subgoal 1:

Variables: L K J N M
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L |- trm M}*
H4 : {L |- trm N}*
H5 : {K |- pr1 M M}
============================
 {K |- pr1 (app M N) (app M N)}

Subgoal 2 is:
 {K |- pr1 (abs R) (abs R)}

Subgoal 3 is:
 {K |- pr1 A A}

pr1_rfl < apply IH to H1 H4.
Subgoal 1:

Variables: L K J N M
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L |- trm M}*
H4 : {L |- trm N}*
H5 : {K |- pr1 M M}
H6 : {K |- pr1 N N}
============================
 {K |- pr1 (app M N) (app M N)}

Subgoal 2 is:
 {K |- pr1 (abs R) (abs R)}

Subgoal 3 is:
 {K |- pr1 A A}

pr1_rfl < search.
Subgoal 2:

Variables: L K J R
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L, trm n1 |- trm (R n1)}*
============================
 {K |- pr1 (abs R) (abs R)}

Subgoal 3 is:
 {K |- pr1 A A}

pr1_rfl < apply IH to _ H3.
Subgoal 2:

Variables: L K J R
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L, trm n1 |- trm (R n1)}*
H4 : {K, pr1 n1 n1 |- pr1 (R n1) (R n1)}
============================
 {K |- pr1 (abs R) (abs R)}

Subgoal 3 is:
 {K |- pr1 A A}

pr1_rfl < search.
Subgoal 3:

Variables: A L K J F
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L, [F] |- trm A}*
H4 : member F L
============================
 {K |- pr1 A A}

pr1_rfl < apply trm_worlds to H1 H4.
Subgoal 3:

Variables: A L K J A1
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs L K J
H3 : {L, [trm A1] |- trm A}*
H4 : member (trm A1) L
H5 : name A1
H6 : member (pr1 A1 A1) K
H7 : member (cd1 A1 A1) J
H8 : member (notabs A1) J
============================
 {K |- pr1 A A}

pr1_rfl < case H5.
Subgoal 3:

Variables: A L K J
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs (L n1) (K n1) (J n1)
H3 : {L n1, [trm n1] |- trm (A n1)}*
H4 : member (trm n1) (L n1)
H6 : member (pr1 n1 n1) (K n1)
H7 : member (cd1 n1 n1) (J n1)
H8 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 (A n1) (A n1)}

pr1_rfl < case H3.
Subgoal 3:

Variables: L K J
IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A}
H1 : ctxs (L n1) (K n1) (J n1)
H4 : member (trm n1) (L n1)
H6 : member (pr1 n1 n1) (K n1)
H7 : member (cd1 n1 n1) (J n1)
H8 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 n1 n1}

pr1_rfl < search.
Proof completed.
Abella < Theorem cd1_unique : 
forall A B C L K J, ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.


============================
 forall A B C L K J, ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C

cd1_unique < induction on 2.

IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
============================
 forall A B C L K J, ctxs L K J -> {J |- cd1 A B}@ -> {J |- cd1 A C} -> B = C

cd1_unique < intros.

Variables: A B C L K J
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H2 : {J |- cd1 A B}@
H3 : {J |- cd1 A C}
============================
 B = C

cd1_unique < case H2.
Subgoal 1:

Variables: C L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 (app T1 S1) C}
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
============================
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H3.
Subgoal 1.1:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J |- notabs T1}
H8 : {J |- cd1 T1 T3}
H9 : {J |- cd1 S1 S3}
============================
 app T2 S2 = app T3 S3

Subgoal 1.2 is:
 app T2 S2 = T3 S3

Subgoal 1.3 is:
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply IH to H1 H5 H8.
Subgoal 1.1:

Variables: L K J S2 S1 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T3}*
H6 : {J |- cd1 S1 S2}*
H7 : {J |- notabs T1}
H8 : {J |- cd1 T1 T3}
H9 : {J |- cd1 S1 S3}
============================
 app T3 S2 = app T3 S3

Subgoal 1.2 is:
 app T2 S2 = T3 S3

Subgoal 1.3 is:
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply IH to H1 H6 H9.
Subgoal 1.1:

Variables: L K J S1 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T3}*
H6 : {J |- cd1 S1 S3}*
H7 : {J |- notabs T1}
H8 : {J |- cd1 T1 T3}
H9 : {J |- cd1 S1 S3}
============================
 app T3 S3 = app T3 S3

Subgoal 1.2 is:
 app T2 S2 = T3 S3

Subgoal 1.3 is:
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < search.
Subgoal 1.2:

Variables: L K J S2 S1 T2 S3 T3 T4
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs (abs T4)}*
H5 : {J |- cd1 (abs T4) T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J |- cd1 (abs T4) (abs T3)}
H8 : {J |- cd1 S1 S3}
============================
 app T2 S2 = T3 S3

Subgoal 1.3 is:
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply notabs_abs_absurd to H1 H4.
Subgoal 1.3:

Variables: C L K J S2 S1 T2 T1 F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J, [F] |- cd1 (app T1 S1) C}
H8 : member F J
============================
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply cd_worlds to H1 H8.
Subgoal 1.3:

Variables: C L K J S2 S1 T2 T1 F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J, [F] |- cd1 (app T1 S1) C}
H8 : member F J
H9 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H9.
Subgoal 1.3.1:

Variables: C L K J S2 S1 T2 T1 B1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J, [cd1 B1 B1] |- cd1 (app T1 S1) C}
H8 : member (cd1 B1 B1) J
H10 : name B1
H11 : member (trm B1) L
H12 : member (pr1 B1 B1) K
H13 : member (notabs B1) J
============================
 app T2 S2 = C

Subgoal 1.3.2 is:
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H10.
Subgoal 1.3.1:

Variables: C L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {J n1 |- notabs (T1 n1)}*
H5 : {J n1 |- cd1 (T1 n1) (T2 n1)}*
H6 : {J n1 |- cd1 (S1 n1) (S2 n1)}*
H7 : {J n1, [cd1 n1 n1] |- cd1 (app (T1 n1) (S1 n1)) (C n1)}
H8 : member (cd1 n1 n1) (J n1)
H11 : member (trm n1) (L n1)
H12 : member (pr1 n1 n1) (K n1)
H13 : member (notabs n1) (J n1)
============================
 app (T2 n1) (S2 n1) = C n1

Subgoal 1.3.2 is:
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H7.
Subgoal 1.3.2:

Variables: C L K J S2 S1 T2 T1 A1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J, [notabs A1] |- cd1 (app T1 S1) C}
H8 : member (notabs A1) J
H10 : name A1
H11 : member (trm A1) L
H12 : member (pr1 A1 A1) K
H13 : member (cd1 A1 A1) J
============================
 app T2 S2 = C

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H10.
Subgoal 1.3.2:

Variables: C L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {J n1 |- notabs (T1 n1)}*
H5 : {J n1 |- cd1 (T1 n1) (T2 n1)}*
H6 : {J n1 |- cd1 (S1 n1) (S2 n1)}*
H7 : {J n1, [notabs n1] |- cd1 (app (T1 n1) (S1 n1)) (C n1)}
H8 : member (notabs n1) (J n1)
H11 : member (trm n1) (L n1)
H12 : member (pr1 n1 n1) (K n1)
H13 : member (cd1 n1 n1) (J n1)
============================
 app (T2 n1) (S2 n1) = C n1

Subgoal 2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H7.
Subgoal 2:

Variables: C L K J S2 S1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 (abs S1) C}
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
============================
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H3.
Subgoal 2.1:

Variables: L K J S2 S1 S3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S3 n1)}
============================
 abs S2 = abs S3

Subgoal 2.2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply IH to _ H4 H5.
Subgoal 2.1:

Variables: L K J S1 S3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S3 n1)}*
H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S3 n1)}
============================
 abs (z1\S3 z1) = abs S3

Subgoal 2.2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < search.
Subgoal 2.2:

Variables: C L K J S2 S1 F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {J, [F] |- cd1 (abs S1) C}
H6 : member F J
============================
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply cd_worlds to H1 H6.
Subgoal 2.2:

Variables: C L K J S2 S1 F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {J, [F] |- cd1 (abs S1) C}
H6 : member F J
H7 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H7.
Subgoal 2.2.1:

Variables: C L K J S2 S1 B1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {J, [cd1 B1 B1] |- cd1 (abs S1) C}
H6 : member (cd1 B1 B1) J
H8 : name B1
H9 : member (trm B1) L
H10 : member (pr1 B1 B1) K
H11 : member (notabs B1) J
============================
 abs S2 = C

Subgoal 2.2.2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H8.
Subgoal 2.2.1:

Variables: C L K J S2 S1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n2) (K n2) (J n2)
H4 : {J n2, notabs n1, cd1 n1 n1 |- cd1 (S1 n2 n1) (S2 n2 n1)}*
H5 : {J n2, [cd1 n2 n2] |- cd1 (abs (S1 n2)) (C n2)}
H6 : member (cd1 n2 n2) (J n2)
H9 : member (trm n2) (L n2)
H10 : member (pr1 n2 n2) (K n2)
H11 : member (notabs n2) (J n2)
============================
 abs (S2 n2) = C n2

Subgoal 2.2.2 is:
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H5.
Subgoal 2.2.2:

Variables: C L K J S2 S1 A1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {J, [notabs A1] |- cd1 (abs S1) C}
H6 : member (notabs A1) J
H8 : name A1
H9 : member (trm A1) L
H10 : member (pr1 A1 A1) K
H11 : member (cd1 A1 A1) J
============================
 abs S2 = C

Subgoal 3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H5.
Subgoal 3:

Variables: C L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 (app (abs T1) S1) C}
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
============================
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H3.
Subgoal 3.1:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J |- notabs (abs T1)}
H7 : {J |- cd1 (abs T1) T3}
H8 : {J |- cd1 S1 S3}
============================
 T2 S2 = app T3 S3

Subgoal 3.2 is:
 T2 S2 = T3 S3

Subgoal 3.3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply notabs_abs_absurd to H1 H6.
Subgoal 3.2:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J |- cd1 (abs T1) (abs T3)}
H7 : {J |- cd1 S1 S3}
============================
 T2 S2 = T3 S3

Subgoal 3.3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply IH to H1 H4 H6.
Subgoal 3.2:

Variables: L K J S2 S1 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T3)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J |- cd1 (abs T1) (abs T3)}
H7 : {J |- cd1 S1 S3}
============================
 T3 S2 = T3 S3

Subgoal 3.3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply IH to H1 H5 H7.
Subgoal 3.2:

Variables: L K J S1 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T3)}*
H5 : {J |- cd1 S1 S3}*
H6 : {J |- cd1 (abs T1) (abs T3)}
H7 : {J |- cd1 S1 S3}
============================
 T3 S3 = T3 S3

Subgoal 3.3 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < search.
Subgoal 3.3:

Variables: C L K J S2 S1 T2 T1 F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J, [F] |- cd1 (app (abs T1) S1) C}
H7 : member F J
============================
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < apply cd_worlds to H1 H7.
Subgoal 3.3:

Variables: C L K J S2 S1 T2 T1 F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J, [F] |- cd1 (app (abs T1) S1) C}
H7 : member F J
H8 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H8.
Subgoal 3.3.1:

Variables: C L K J S2 S1 T2 T1 B1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J, [cd1 B1 B1] |- cd1 (app (abs T1) S1) C}
H7 : member (cd1 B1 B1) J
H9 : name B1
H10 : member (trm B1) L
H11 : member (pr1 B1 B1) K
H12 : member (notabs B1) J
============================
 T2 S2 = C

Subgoal 3.3.2 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H9.
Subgoal 3.3.1:

Variables: C L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {J n1 |- cd1 (abs (T1 n1)) (abs (T2 n1))}*
H5 : {J n1 |- cd1 (S1 n1) (S2 n1)}*
H6 : {J n1, [cd1 n1 n1] |- cd1 (app (abs (T1 n1)) (S1 n1)) (C n1)}
H7 : member (cd1 n1 n1) (J n1)
H10 : member (trm n1) (L n1)
H11 : member (pr1 n1 n1) (K n1)
H12 : member (notabs n1) (J n1)
============================
 T2 n1 (S2 n1) = C n1

Subgoal 3.3.2 is:
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H6.
Subgoal 3.3.2:

Variables: C L K J S2 S1 T2 T1 A1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J, [notabs A1] |- cd1 (app (abs T1) S1) C}
H7 : member (notabs A1) J
H9 : name A1
H10 : member (trm A1) L
H11 : member (pr1 A1 A1) K
H12 : member (cd1 A1 A1) J
============================
 T2 S2 = C

Subgoal 4 is:
 B = C

cd1_unique < case H6.
Subgoal 4:

Variables: A B C L K J F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 A C}
H4 : {J, [F] |- cd1 A B}*
H5 : member F J
============================
 B = C

cd1_unique < apply cd_worlds to H1 H5.
Subgoal 4:

Variables: A B C L K J F
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 A C}
H4 : {J, [F] |- cd1 A B}*
H5 : member F J
H6 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 B = C

cd1_unique < case H6.
Subgoal 4.1:

Variables: A B C L K J B1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 A C}
H4 : {J, [cd1 B1 B1] |- cd1 A B}*
H5 : member (cd1 B1 B1) J
H7 : name B1
H8 : member (trm B1) L
H9 : member (pr1 B1 B1) K
H10 : member (notabs B1) J
============================
 B = C

Subgoal 4.2 is:
 B = C

cd1_unique < case H7.
Subgoal 4.1:

Variables: A B C L K J
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H3 : {J n1 |- cd1 (A n1) (C n1)}
H4 : {J n1, [cd1 n1 n1] |- cd1 (A n1) (B n1)}*
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
============================
 B n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < case H4.
Subgoal 4.1:

Variables: C L K J
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H3 : {J n1 |- cd1 n1 (C n1)}
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
============================
 n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < case H3.
Subgoal 4.1:

Variables: C L K J F1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
H11 : {J n1, [F1 n1] |- cd1 n1 (C n1)}
H12 : member (F1 n1) (J n1)
============================
 n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < apply cd_worlds to H1 H12.
Subgoal 4.1:

Variables: C L K J F1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
H11 : {J n1, [F1 n1] |- cd1 n1 (C n1)}
H12 : member (F1 n1) (J n1)
H13 : (exists A B, F1 n1 = cd1 A B /\ name A /\ A = B /\
           member (trm A) (L n1) /\ member (pr1 A A) (K n1) /\
           member (notabs A) (J n1)) \/
        (exists A, F1 n1 = notabs A /\ name A /\ member (trm A) (L n1) /\
             member (pr1 A A) (K n1) /\ member (cd1 A A) (J n1))
============================
 n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < case H13.
Subgoal 4.1.1:

Variables: C L K J B2
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
H11 : {J n1, [cd1 (B2 n1) (B2 n1)] |- cd1 n1 (C n1)}
H12 : member (cd1 (B2 n1) (B2 n1)) (J n1)
H14 : name (B2 n1)
H15 : member (trm (B2 n1)) (L n1)
H16 : member (pr1 (B2 n1) (B2 n1)) (K n1)
H17 : member (notabs (B2 n1)) (J n1)
============================
 n1 = C n1

Subgoal 4.1.2 is:
 n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < case H11.
Subgoal 4.1.1:

Variables: L K J
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
H12 : member (cd1 n1 n1) (J n1)
H14 : name n1
H15 : member (trm n1) (L n1)
H16 : member (pr1 n1 n1) (K n1)
H17 : member (notabs n1) (J n1)
============================
 n1 = n1

Subgoal 4.1.2 is:
 n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < search.
Subgoal 4.1.2:

Variables: C L K J A2
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs (L n1) (K n1) (J n1)
H5 : member (cd1 n1 n1) (J n1)
H8 : member (trm n1) (L n1)
H9 : member (pr1 n1 n1) (K n1)
H10 : member (notabs n1) (J n1)
H11 : {J n1, [notabs (A2 n1)] |- cd1 n1 (C n1)}
H12 : member (notabs (A2 n1)) (J n1)
H14 : name (A2 n1)
H15 : member (trm (A2 n1)) (L n1)
H16 : member (pr1 (A2 n1) (A2 n1)) (K n1)
H17 : member (cd1 (A2 n1) (A2 n1)) (J n1)
============================
 n1 = C n1

Subgoal 4.2 is:
 B = C

cd1_unique < case H11.
Subgoal 4.2:

Variables: A B C L K J A1
IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} ->
       B =
     C
H1 : ctxs L K J
H3 : {J |- cd1 A C}
H4 : {J, [notabs A1] |- cd1 A B}*
H5 : member (notabs A1) J
H7 : name A1
H8 : member (trm A1) L
H9 : member (pr1 A1 A1) K
H10 : member (cd1 A1 A1) J
============================
 B = C

cd1_unique < case H4.
Proof completed.
Abella < Theorem cd1_exists : 
forall A L K J, ctxs L K J -> {L |- trm A} -> (exists B, {J |- cd1 A B}).


============================
 forall A L K J, ctxs L K J -> {L |- trm A} -> (exists B, {J |- cd1 A B})

cd1_exists < induction on 2.

IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
============================
 forall A L K J, ctxs L K J -> {L |- trm A}@ -> (exists B, {J |- cd1 A B})

cd1_exists < intros.

Variables: A L K J
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H2 : {L |- trm A}@
============================
 exists B, {J |- cd1 A B}

cd1_exists < case H2.
Subgoal 1:

Variables: L K J N M
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L |- trm M}*
H4 : {L |- trm N}*
============================
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < apply IH to H1 H3.
Subgoal 1:

Variables: L K J N M B
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L |- trm M}*
H4 : {L |- trm N}*
H5 : {J |- cd1 M B}
============================
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < apply IH to H1 H4.
Subgoal 1:

Variables: L K J N M B B1
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L |- trm M}*
H4 : {L |- trm N}*
H5 : {J |- cd1 M B}
H6 : {J |- cd1 N B1}
============================
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < case H3.
Subgoal 1.1:

Variables: L K J N B B1 N1 M1
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : {L |- trm N}*
H5 : {J |- cd1 (app M1 N1) B}
H6 : {J |- cd1 N B1}
H7 : {L |- trm M1}*
H8 : {L |- trm N1}*
============================
 exists B, {J |- cd1 (app (app M1 N1) N) B}

Subgoal 1.2 is:
 exists B, {J |- cd1 (app (abs R) N) B}

Subgoal 1.3 is:
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < search.
Subgoal 1.2:

Variables: L K J N B B1 R
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : {L |- trm N}*
H5 : {J |- cd1 (abs R) B}
H6 : {J |- cd1 N B1}
H7 : {L, trm n1 |- trm (R n1)}*
============================
 exists B, {J |- cd1 (app (abs R) N) B}

Subgoal 1.3 is:
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < apply IH to _ H7.
Subgoal 1.2:

Variables: L K J N B B1 R B2
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : {L |- trm N}*
H5 : {J |- cd1 (abs R) B}
H6 : {J |- cd1 N B1}
H7 : {L, trm n1 |- trm (R n1)}*
H8 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (B2 n1)}
============================
 exists B, {J |- cd1 (app (abs R) N) B}

Subgoal 1.3 is:
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < search.
Subgoal 1.3:

Variables: L K J N M B B1 F
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : {L |- trm N}*
H5 : {J |- cd1 M B}
H6 : {J |- cd1 N B1}
H7 : {L, [F] |- trm M}*
H8 : member F L
============================
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < apply trm_worlds to H1 H8.
Subgoal 1.3:

Variables: L K J N M B B1 A1
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : {L |- trm N}*
H5 : {J |- cd1 M B}
H6 : {J |- cd1 N B1}
H7 : {L, [trm A1] |- trm M}*
H8 : member (trm A1) L
H9 : name A1
H10 : member (pr1 A1 A1) K
H11 : member (cd1 A1 A1) J
H12 : member (notabs A1) J
============================
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < case H7.
Subgoal 1.3:

Variables: L K J N M B B1
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : {L |- trm N}*
H5 : {J |- cd1 M B}
H6 : {J |- cd1 N B1}
H8 : member (trm M) L
H9 : name M
H10 : member (pr1 M M) K
H11 : member (cd1 M M) J
H12 : member (notabs M) J
============================
 exists B, {J |- cd1 (app M N) B}

Subgoal 2 is:
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < search.
Subgoal 2:

Variables: L K J R
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L, trm n1 |- trm (R n1)}*
============================
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < apply IH to _ H3.
Subgoal 2:

Variables: L K J R B
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L, trm n1 |- trm (R n1)}*
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (B n1)}
============================
 exists B, {J |- cd1 (abs R) B}

Subgoal 3 is:
 exists B, {J |- cd1 A B}

cd1_exists < search.
Subgoal 3:

Variables: A L K J F
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L, [F] |- trm A}*
H4 : member F L
============================
 exists B, {J |- cd1 A B}

cd1_exists < apply trm_worlds to H1 H4.
Subgoal 3:

Variables: A L K J A1
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H3 : {L, [trm A1] |- trm A}*
H4 : member (trm A1) L
H5 : name A1
H6 : member (pr1 A1 A1) K
H7 : member (cd1 A1 A1) J
H8 : member (notabs A1) J
============================
 exists B, {J |- cd1 A B}

cd1_exists < case H3.
Subgoal 3:

Variables: A L K J
IH : forall A L K J, ctxs L K J -> {L |- trm A}* ->
       (exists B, {J |- cd1 A B})
H1 : ctxs L K J
H4 : member (trm A) L
H5 : name A
H6 : member (pr1 A A) K
H7 : member (cd1 A A) J
H8 : member (notabs A) J
============================
 exists B, {J |- cd1 A B}

cd1_exists < search.
Proof completed.
Abella < Theorem pr1_name : 
forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> name A -> B = A.


============================
 forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> name A -> B = A

pr1_name < intros.

Variables: A B L K J
H1 : ctxs L K J
H2 : {K |- pr1 A B}
H3 : name A
============================
 B = A

pr1_name < case H3.

Variables: B L K J
H1 : ctxs (L n1) (K n1) (J n1)
H2 : {K n1 |- pr1 n1 (B n1)}
============================
 B n1 = n1

pr1_name < case H2.

Variables: B L K J F
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {K n1, [F n1] |- pr1 n1 (B n1)}
H5 : member (F n1) (K n1)
============================
 B n1 = n1

pr1_name < apply pr1_worlds to H1 H5.

Variables: B L K J B1
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {K n1, [pr1 (B1 n1) (B1 n1)] |- pr1 n1 (B n1)}
H5 : member (pr1 (B1 n1) (B1 n1)) (K n1)
H6 : name (B1 n1)
H7 : member (trm (B1 n1)) (L n1)
H8 : member (cd1 (B1 n1) (B1 n1)) (J n1)
H9 : member (notabs (B1 n1)) (J n1)
============================
 B n1 = n1

pr1_name < case H4.

Variables: L K J
H1 : ctxs (L n1) (K n1) (J n1)
H5 : member (pr1 n1 n1) (K n1)
H6 : name n1
H7 : member (trm n1) (L n1)
H8 : member (cd1 n1 n1) (J n1)
H9 : member (notabs n1) (J n1)
============================
 n1 = n1

pr1_name < search.
Proof completed.
Abella < Theorem pr1_abs : 
forall R B L K J, ctxs L K J -> {K |- pr1 (abs R) B} -> (exists S, B = abs S).


============================
 forall R B L K J, ctxs L K J -> {K |- pr1 (abs R) B} ->
   (exists S, B = abs S)

pr1_abs < intros.

Variables: R B L K J
H1 : ctxs L K J
H2 : {K |- pr1 (abs R) B}
============================
 exists S, B = abs S

pr1_abs < case H2.
Subgoal 1:

Variables: R L K J S2
H1 : ctxs L K J
H3 : {K, pr1 n1 n1 |- pr1 (R n1) (S2 n1)}
============================
 exists S, abs S2 = abs S

Subgoal 2 is:
 exists S, B = abs S

pr1_abs < search.
Subgoal 2:

Variables: R B L K J F
H1 : ctxs L K J
H3 : {K, [F] |- pr1 (abs R) B}
H4 : member F K
============================
 exists S, B = abs S

pr1_abs < apply pr1_worlds to H1 H4.
Subgoal 2:

Variables: R B L K J B1
H1 : ctxs L K J
H3 : {K, [pr1 B1 B1] |- pr1 (abs R) B}
H4 : member (pr1 B1 B1) K
H5 : name B1
H6 : member (trm B1) L
H7 : member (cd1 B1 B1) J
H8 : member (notabs B1) J
============================
 exists S, B = abs S

pr1_abs < case H5.
Subgoal 2:

Variables: R B L K J
H1 : ctxs (L n1) (K n1) (J n1)
H3 : {K n1, [pr1 n1 n1] |- pr1 (abs (R n1)) (B n1)}
H4 : member (pr1 n1 n1) (K n1)
H6 : member (trm n1) (L n1)
H7 : member (cd1 n1 n1) (J n1)
H8 : member (notabs n1) (J n1)
============================
 exists S, B n1 = abs S

pr1_abs < case H3.
Proof completed.
Abella < Theorem pre_pr1_subst_lem : 
forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
  {K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} ->
  {K |- pr1 (A1 B1) (A2 B2)}.


============================
 forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
   {K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} ->
   {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < induction on 2.

IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
============================
 forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
   {K, pr1 x x |- pr1 (A1 x) (A2 x)}@ -> {K |- pr1 B1 B2} ->
   {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < intros.

Variables: A1 A2 B1 B2 L K J
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H2 : {K, pr1 n1 n1 |- pr1 (A1 n1) (A2 n1)}@
H3 : {K |- pr1 B1 B2}
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < case H2.
Subgoal 1:

Variables: B1 B2 L K J S2 S1 T2 T1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (T1 n1) (T2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
============================
 {K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}

Subgoal 2 is:
 {K |- pr1 (abs (S1 B1)) (abs (S2 B2))}

Subgoal 3 is:
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < apply IH to H1 H4 H3.
Subgoal 1:

Variables: B1 B2 L K J S2 S1 T2 T1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (T1 n1) (T2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
H6 : {K |- pr1 (T1 B1) (T2 B2)}
============================
 {K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}

Subgoal 2 is:
 {K |- pr1 (abs (S1 B1)) (abs (S2 B2))}

Subgoal 3 is:
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < apply IH to H1 H5 H3.
Subgoal 1:

Variables: B1 B2 L K J S2 S1 T2 T1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (T1 n1) (T2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
H6 : {K |- pr1 (T1 B1) (T2 B2)}
H7 : {K |- pr1 (S1 B1) (S2 B2)}
============================
 {K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}

Subgoal 2 is:
 {K |- pr1 (abs (S1 B1)) (abs (S2 B2))}

Subgoal 3 is:
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < search.
Subgoal 2:

Variables: B1 B2 L K J S2 S1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1, pr1 n2 n2 |- pr1 (S1 n1 n2) (S2 n1 n2)}*
============================
 {K |- pr1 (abs (S1 B1)) (abs (S2 B2))}

Subgoal 3 is:
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < apply IH to _ H4 H3.
Subgoal 2:

Variables: B1 B2 L K J S2 S1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1, pr1 n2 n2 |- pr1 (S1 n1 n2) (S2 n1 n2)}*
H5 : {K, pr1 n2 n2 |- pr1 (S1 B1 n2) (S2 B2 n2)}
============================
 {K |- pr1 (abs (S1 B1)) (abs (S2 B2))}

Subgoal 3 is:
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < search.
Subgoal 3:

Variables: B1 B2 L K J S2 S1 T2 T1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (abs (T1 n1)) (abs (T2 n1))}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
============================
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < apply IH to H1 H4 H3.
Subgoal 3:

Variables: B1 B2 L K J S2 S1 T2 T1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (abs (T1 n1)) (abs (T2 n1))}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
H6 : {K |- pr1 (abs (T1 B1)) (abs (T2 B2))}
============================
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < apply IH to H1 H5 H3.
Subgoal 3:

Variables: B1 B2 L K J S2 S1 T2 T1
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (abs (T1 n1)) (abs (T2 n1))}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}*
H6 : {K |- pr1 (abs (T1 B1)) (abs (T2 B2))}
H7 : {K |- pr1 (S1 B1) (S2 B2)}
============================
 {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}

Subgoal 4 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < search.
Subgoal 4:

Variables: A1 A2 B1 B2 L K J F
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1, [F n1] |- pr1 (A1 n1) (A2 n1)}*
H5 : member (F n1) (pr1 n1 n1 :: K)
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < case H5.
Subgoal 4.1:

Variables: A1 A2 B1 B2 L K J
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1, [pr1 n1 n1] |- pr1 (A1 n1) (A2 n1)}*
============================
 {K |- pr1 (A1 B1) (A2 B2)}

Subgoal 4.2 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < case H4.
Subgoal 4.1:

Variables: B1 B2 L K J
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
============================
 {K |- pr1 B1 B2}

Subgoal 4.2 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < search.
Subgoal 4.2:

Variables: A1 A2 B1 B2 L K J F
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1, [F n1] |- pr1 (A1 n1) (A2 n1)}*
H6 : member (F n1) K
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < apply pr1_worlds to H1 H6.
Subgoal 4.2:

Variables: A1 A2 B1 B2 L K J B
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1, [pr1 (B n1) (B n1)] |- pr1 (A1 n1) (A2 n1)}*
H6 : member (pr1 (B n1) (B n1)) K
H7 : name (B n1)
H8 : member (trm (B n1)) L
H9 : member (cd1 (B n1) (B n1)) J
H10 : member (notabs (B n1)) J
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pre_pr1_subst_lem < case H4.
Subgoal 4.2:

Variables: A2 B1 B2 L K J
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H6 : member (pr1 (A2 n1) (A2 n1)) K
H7 : name (A2 n1)
H8 : member (trm (A2 n1)) L
H9 : member (cd1 (A2 n1) (A2 n1)) J
H10 : member (notabs (A2 n1)) J
============================
 {K |- pr1 (A2 B1) (A2 B2)}

pre_pr1_subst_lem < case H7.
Subgoal 4.2.1:

Variables: B1 B2 L K J
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs (L n2) (K n2) (J n2)
H3 : {K n2 |- pr1 (B1 n2) (B2 n2)}
H6 : member (pr1 n2 n2) (K n2)
H8 : member (trm n2) (L n2)
H9 : member (cd1 n2 n2) (J n2)
H10 : member (notabs n2) (J n2)
============================
 {K n2 |- pr1 n2 n2}

Subgoal 4.2.2 is:
 {K |- pr1 B1 B2}

pre_pr1_subst_lem < search.
Subgoal 4.2.2:

Variables: B1 B2 L K J
IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J ->
       {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} ->
       {K |- pr1 (A1 B1) (A2 B2)}
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H6 : member (pr1 n1 n1) K
H8 : member (trm n1) L
H9 : member (cd1 n1 n1) J
H10 : member (notabs n1) J
============================
 {K |- pr1 B1 B2}

pre_pr1_subst_lem < search.
Proof completed.
Abella < Theorem pr1_subst_lem : 
forall A1 A2 B1 B2 L K J, ctxs L K J -> {K |- pr1 (abs A1) (abs A2)} ->
  {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)}.


============================
 forall A1 A2 B1 B2 L K J, ctxs L K J -> {K |- pr1 (abs A1) (abs A2)} ->
   {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)}

pr1_subst_lem < intros.

Variables: A1 A2 B1 B2 L K J
H1 : ctxs L K J
H2 : {K |- pr1 (abs A1) (abs A2)}
H3 : {K |- pr1 B1 B2}
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pr1_subst_lem < case H2.
Subgoal 1:

Variables: A1 A2 B1 B2 L K J
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (A1 n1) (A2 n1)}
============================
 {K |- pr1 (A1 B1) (A2 B2)}

Subgoal 2 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pr1_subst_lem < apply pre_pr1_subst_lem to H1 H4 H3.
Subgoal 1:

Variables: A1 A2 B1 B2 L K J
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, pr1 n1 n1 |- pr1 (A1 n1) (A2 n1)}
H5 : {K |- pr1 (A1 B1) (A2 B2)}
============================
 {K |- pr1 (A1 B1) (A2 B2)}

Subgoal 2 is:
 {K |- pr1 (A1 B1) (A2 B2)}

pr1_subst_lem < search.
Subgoal 2:

Variables: A1 A2 B1 B2 L K J F
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, [F] |- pr1 (abs A1) (abs A2)}
H5 : member F K
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pr1_subst_lem < apply pr1_worlds to H1 H5.
Subgoal 2:

Variables: A1 A2 B1 B2 L K J B
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : {K, [pr1 B B] |- pr1 (abs A1) (abs A2)}
H5 : member (pr1 B B) K
H6 : name B
H7 : member (trm B) L
H8 : member (cd1 B B) J
H9 : member (notabs B) J
============================
 {K |- pr1 (A1 B1) (A2 B2)}

pr1_subst_lem < case H4.
Subgoal 2:

Variables: A2 B1 B2 L K J
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H5 : member (pr1 (abs A2) (abs A2)) K
H6 : name (abs A2)
H7 : member (trm (abs A2)) L
H8 : member (cd1 (abs A2) (abs A2)) J
H9 : member (notabs (abs A2)) J
============================
 {K |- pr1 (A2 B1) (A2 B2)}

pr1_subst_lem < case H6.
Proof completed.
Abella < Theorem cd1_pr1_triangle : 
forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C} ->
  {K |- pr1 B C}.


============================
 forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C} ->
   {K |- pr1 B C}

cd1_pr1_triangle < induction on 3.

IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
============================
 forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}@ ->
   {K |- pr1 B C}

cd1_pr1_triangle < intros.

Variables: A B C L K J
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 A B}
H3 : {J |- cd1 A C}@
============================
 {K |- pr1 B C}

cd1_pr1_triangle < case H3.
Subgoal 1:

Variables: B L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 (app T1 S1) B}
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
============================
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H2.
Subgoal 1.1:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 T1 T3}
H8 : {K |- pr1 S1 S3}
============================
 {K |- pr1 (app T3 S3) (app T2 S2)}

Subgoal 1.2 is:
 {K |- pr1 (T3 S3) (app T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to H1 H7 H5.
Subgoal 1.1:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 T1 T3}
H8 : {K |- pr1 S1 S3}
H9 : {K |- pr1 T3 T2}
============================
 {K |- pr1 (app T3 S3) (app T2 S2)}

Subgoal 1.2 is:
 {K |- pr1 (T3 S3) (app T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to H1 H8 H6.
Subgoal 1.1:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 T1 T3}
H8 : {K |- pr1 S1 S3}
H9 : {K |- pr1 T3 T2}
H10 : {K |- pr1 S3 S2}
============================
 {K |- pr1 (app T3 S3) (app T2 S2)}

Subgoal 1.2 is:
 {K |- pr1 (T3 S3) (app T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < search.
Subgoal 1.2:

Variables: L K J S2 S1 T2 S3 T3 T4
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- notabs (abs T4)}*
H5 : {J |- cd1 (abs T4) T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 (abs T4) (abs T3)}
H8 : {K |- pr1 S1 S3}
============================
 {K |- pr1 (T3 S3) (app T2 S2)}

Subgoal 1.3 is:
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply notabs_abs_absurd to H1 H4.
Subgoal 1.3:

Variables: B L K J S2 S1 T2 T1 F
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K, [F] |- pr1 (app T1 S1) B}
H8 : member F K
============================
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply pr1_worlds to H1 H8.
Subgoal 1.3:

Variables: B L K J S2 S1 T2 T1 B1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K, [pr1 B1 B1] |- pr1 (app T1 S1) B}
H8 : member (pr1 B1 B1) K
H9 : name B1
H10 : member (trm B1) L
H11 : member (cd1 B1 B1) J
H12 : member (notabs B1) J
============================
 {K |- pr1 B (app T2 S2)}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H9.
Subgoal 1.3:

Variables: B L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {J n1 |- notabs (T1 n1)}*
H5 : {J n1 |- cd1 (T1 n1) (T2 n1)}*
H6 : {J n1 |- cd1 (S1 n1) (S2 n1)}*
H7 : {K n1, [pr1 n1 n1] |- pr1 (app (T1 n1) (S1 n1)) (B n1)}
H8 : member (pr1 n1 n1) (K n1)
H10 : member (trm n1) (L n1)
H11 : member (cd1 n1 n1) (J n1)
H12 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 (B n1) (app (T2 n1) (S2 n1))}

Subgoal 2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H7.
Subgoal 2:

Variables: B L K J S2 S1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 (abs S1) B}
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
============================
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H2.
Subgoal 2.1:

Variables: L K J S2 S1 S3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S3 n1)}
============================
 {K |- pr1 (abs S3) (abs S2)}

Subgoal 2.2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to _ H5 H4.
Subgoal 2.1:

Variables: L K J S2 S1 S3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S3 n1)}
H6 : {K, pr1 n1 n1 |- pr1 (S3 n1) (S2 n1)}
============================
 {K |- pr1 (abs S3) (abs S2)}

Subgoal 2.2 is:
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < search.
Subgoal 2.2:

Variables: B L K J S2 S1 F
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {K, [F] |- pr1 (abs S1) B}
H6 : member F K
============================
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply pr1_worlds to H1 H6.
Subgoal 2.2:

Variables: B L K J S2 S1 B1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {K, [pr1 B1 B1] |- pr1 (abs S1) B}
H6 : member (pr1 B1 B1) K
H7 : name B1
H8 : member (trm B1) L
H9 : member (cd1 B1 B1) J
H10 : member (notabs B1) J
============================
 {K |- pr1 B (abs S2)}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H7.
Subgoal 2.2:

Variables: B L K J S2 S1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs (L n2) (K n2) (J n2)
H4 : {J n2, notabs n1, cd1 n1 n1 |- cd1 (S1 n2 n1) (S2 n2 n1)}*
H5 : {K n2, [pr1 n2 n2] |- pr1 (abs (S1 n2)) (B n2)}
H6 : member (pr1 n2 n2) (K n2)
H8 : member (trm n2) (L n2)
H9 : member (cd1 n2 n2) (J n2)
H10 : member (notabs n2) (J n2)
============================
 {K n2 |- pr1 (B n2) (abs (S2 n2))}

Subgoal 3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H5.
Subgoal 3:

Variables: B L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 (app (abs T1) S1) B}
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
============================
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H2.
Subgoal 3.1:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) T3}
H7 : {K |- pr1 S1 S3}
============================
 {K |- pr1 (app T3 S3) (T2 S2)}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H6.
Subgoal 3.1.1:

Variables: L K J S2 S1 T2 T1 S3 S4
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S3}
H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S4 n1)}
============================
 {K |- pr1 (app (abs S4) S3) (T2 S2)}

Subgoal 3.1.2 is:
 {K |- pr1 (app T3 S3) (T2 S2)}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to H1 H7 H5.
Subgoal 3.1.1:

Variables: L K J S2 S1 T2 T1 S3 S4
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S3}
H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S4 n1)}
H9 : {K |- pr1 S3 S2}
============================
 {K |- pr1 (app (abs S4) S3) (T2 S2)}

Subgoal 3.1.2 is:
 {K |- pr1 (app T3 S3) (T2 S2)}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to H1 _ H4.
Subgoal 3.1.1:

Variables: L K J S2 S1 T2 T1 S3 S4
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S3}
H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S4 n1)}
H9 : {K |- pr1 S3 S2}
H10 : {K |- pr1 (abs (z1\S4 z1)) (abs T2)}
============================
 {K |- pr1 (app (abs S4) S3) (T2 S2)}

Subgoal 3.1.2 is:
 {K |- pr1 (app T3 S3) (T2 S2)}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < search.
Subgoal 3.1.2:

Variables: L K J S2 S1 T2 T1 S3 T3 F
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S3}
H8 : {K, [F] |- pr1 (abs T1) T3}
H9 : member F K
============================
 {K |- pr1 (app T3 S3) (T2 S2)}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply pr1_worlds to H1 H9.
Subgoal 3.1.2:

Variables: L K J S2 S1 T2 T1 S3 T3 B1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S3}
H8 : {K, [pr1 B1 B1] |- pr1 (abs T1) T3}
H9 : member (pr1 B1 B1) K
H10 : name B1
H11 : member (trm B1) L
H12 : member (cd1 B1 B1) J
H13 : member (notabs B1) J
============================
 {K |- pr1 (app T3 S3) (T2 S2)}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H10.
Subgoal 3.1.2:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {J n1 |- cd1 (abs (T1 n1)) (abs (T2 n1))}*
H5 : {J n1 |- cd1 (S1 n1) (S2 n1)}*
H7 : {K n1 |- pr1 (S1 n1) (S3 n1)}
H8 : {K n1, [pr1 n1 n1] |- pr1 (abs (T1 n1)) (T3 n1)}
H9 : member (pr1 n1 n1) (K n1)
H11 : member (trm n1) (L n1)
H12 : member (cd1 n1 n1) (J n1)
H13 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 (app (T3 n1) (S3 n1)) (T2 n1 (S2 n1))}

Subgoal 3.2 is:
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H8.
Subgoal 3.2:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T3)}
H7 : {K |- pr1 S1 S3}
============================
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to H1 H7 H5.
Subgoal 3.2:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T3)}
H7 : {K |- pr1 S1 S3}
H8 : {K |- pr1 S3 S2}
============================
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply IH to H1 _ H4.
Subgoal 3.2:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T3)}
H7 : {K |- pr1 S1 S3}
H8 : {K |- pr1 S3 S2}
H9 : {K |- pr1 (abs T3) (abs T2)}
============================
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply pr1_subst_lem to H1 H9 H8.
Subgoal 3.2:

Variables: L K J S2 S1 T2 T1 S3 T3
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T3)}
H7 : {K |- pr1 S1 S3}
H8 : {K |- pr1 S3 S2}
H9 : {K |- pr1 (abs T3) (abs T2)}
H10 : {K |- pr1 (T3 S3) (T2 S2)}
============================
 {K |- pr1 (T3 S3) (T2 S2)}

Subgoal 3.3 is:
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < search.
Subgoal 3.3:

Variables: B L K J S2 S1 T2 T1 F
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K, [F] |- pr1 (app (abs T1) S1) B}
H7 : member F K
============================
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply pr1_worlds to H1 H7.
Subgoal 3.3:

Variables: B L K J S2 S1 T2 T1 B1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K, [pr1 B1 B1] |- pr1 (app (abs T1) S1) B}
H7 : member (pr1 B1 B1) K
H8 : name B1
H9 : member (trm B1) L
H10 : member (cd1 B1 B1) J
H11 : member (notabs B1) J
============================
 {K |- pr1 B (T2 S2)}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H8.
Subgoal 3.3:

Variables: B L K J S2 S1 T2 T1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs (L n1) (K n1) (J n1)
H4 : {J n1 |- cd1 (abs (T1 n1)) (abs (T2 n1))}*
H5 : {J n1 |- cd1 (S1 n1) (S2 n1)}*
H6 : {K n1, [pr1 n1 n1] |- pr1 (app (abs (T1 n1)) (S1 n1)) (B n1)}
H7 : member (pr1 n1 n1) (K n1)
H9 : member (trm n1) (L n1)
H10 : member (cd1 n1 n1) (J n1)
H11 : member (notabs n1) (J n1)
============================
 {K n1 |- pr1 (B n1) (T2 n1 (S2 n1))}

Subgoal 4 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H6.
Subgoal 4:

Variables: A B C L K J F
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 A B}
H4 : {J, [F] |- cd1 A C}*
H5 : member F J
============================
 {K |- pr1 B C}

cd1_pr1_triangle < apply cd_worlds to H1 H5.
Subgoal 4:

Variables: A B C L K J F
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 A B}
H4 : {J, [F] |- cd1 A C}*
H5 : member F J
H6 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\
          member (pr1 A A) K /\ member (notabs A) J) \/
       (exists A, F = notabs A /\ name A /\ member (trm A) L /\
            member (pr1 A A) K /\ member (cd1 A A) J)
============================
 {K |- pr1 B C}

cd1_pr1_triangle < case H6.
Subgoal 4.1:

Variables: A B C L K J B1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 A B}
H4 : {J, [cd1 B1 B1] |- cd1 A C}*
H5 : member (cd1 B1 B1) J
H7 : name B1
H8 : member (trm B1) L
H9 : member (pr1 B1 B1) K
H10 : member (notabs B1) J
============================
 {K |- pr1 B C}

Subgoal 4.2 is:
 {K |- pr1 B C}

cd1_pr1_triangle < case H4.
Subgoal 4.1:

Variables: B C L K J
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 C B}
H5 : member (cd1 C C) J
H7 : name C
H8 : member (trm C) L
H9 : member (pr1 C C) K
H10 : member (notabs C) J
============================
 {K |- pr1 B C}

Subgoal 4.2 is:
 {K |- pr1 B C}

cd1_pr1_triangle < apply pr1_name to H1 H2 H7.
Subgoal 4.1:

Variables: C L K J
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 C C}
H5 : member (cd1 C C) J
H7 : name C
H8 : member (trm C) L
H9 : member (pr1 C C) K
H10 : member (notabs C) J
============================
 {K |- pr1 C C}

Subgoal 4.2 is:
 {K |- pr1 B C}

cd1_pr1_triangle < search.
Subgoal 4.2:

Variables: A B C L K J A1
IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* ->
       {K |- pr1 B C}
H1 : ctxs L K J
H2 : {K |- pr1 A B}
H4 : {J, [notabs A1] |- cd1 A C}*
H5 : member (notabs A1) J
H7 : name A1
H8 : member (trm A1) L
H9 : member (pr1 A1 A1) K
H10 : member (cd1 A1 A1) J
============================
 {K |- pr1 B C}

cd1_pr1_triangle < case H4.
Proof completed.
Abella < Theorem pr1_diamond : 
forall A B1 B2 L K J, ctxs L K J -> {K |- pr1 A B1} -> {K |- pr1 A B2} ->
  (exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}).


============================
 forall A B1 B2 L K J, ctxs L K J -> {K |- pr1 A B1} -> {K |- pr1 A B2} ->
   (exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C})

pr1_diamond < intros.

Variables: A B1 B2 L K J
H1 : ctxs L K J
H2 : {K |- pr1 A B1}
H3 : {K |- pr1 A B2}
============================
 exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}

pr1_diamond < apply pr1_trm to H1 H2.

Variables: A B1 B2 L K J
H1 : ctxs L K J
H2 : {K |- pr1 A B1}
H3 : {K |- pr1 A B2}
H4 : {L |- trm A}
============================
 exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}

pr1_diamond < apply cd1_exists to H1 H4.

Variables: A B1 B2 L K J B
H1 : ctxs L K J
H2 : {K |- pr1 A B1}
H3 : {K |- pr1 A B2}
H4 : {L |- trm A}
H5 : {J |- cd1 A B}
============================
 exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}

pr1_diamond < apply cd1_pr1_triangle to H1 H2 H5.

Variables: A B1 B2 L K J B
H1 : ctxs L K J
H2 : {K |- pr1 A B1}
H3 : {K |- pr1 A B2}
H4 : {L |- trm A}
H5 : {J |- cd1 A B}
H6 : {K |- pr1 B1 B}
============================
 exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}

pr1_diamond < apply cd1_pr1_triangle to H1 H3 H5.

Variables: A B1 B2 L K J B
H1 : ctxs L K J
H2 : {K |- pr1 A B1}
H3 : {K |- pr1 A B2}
H4 : {L |- trm A}
H5 : {J |- cd1 A B}
H6 : {K |- pr1 B1 B}
H7 : {K |- pr1 B2 B}
============================
 exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}

pr1_diamond < search.
Proof completed.
Abella <