Welcome to Abella 2.0.2-parinati

Abella < Specification "unique.elf".
Reading specification "unique.elf"
sig unique.
  type ty lftype.
  type i lfobj.
  type arr lfobj -> lfobj -> lfobj.
  type tm lftype.
  type u lfobj.
  type lam lfobj -> (lfobj -> lfobj) -> lfobj.
  type app lfobj -> lfobj -> lfobj.
  type of lfobj -> lfobj -> lftype.
  type of/u lfobj.
  type of/app lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj.
  type of/lam lfobj -> lfobj -> (lfobj -> lfobj) -> (lfobj -> lfobj -> lfobj) -> lfobj.
end.
module unique.
  (* ty:type *)
  lfisty ty.
  (* i:ty *)
  lfhas i ty.
  (* arr:ty -> ty -> ty *)
  pi lf_1\lfhas lf_1 ty => pi lf_2\lfhas lf_2 ty => lfhas (arr lf_1 lf_2) ty.
  (* tm:type *)
  lfisty tm.
  (* u:tm *)
  lfhas u tm.
  (* lam:ty -> (tm -> tm) -> tm *)
  pi lf_1\lfhas lf_1 ty =>
    pi lf_2\(pi lf_3\lfhas lf_3 tm => lfhas (lf_2 lf_3) tm) =>
      lfhas (lam lf_1 lf_2) tm.
  (* app:tm -> tm -> tm *)
  pi lf_1\lfhas lf_1 tm => pi lf_2\lfhas lf_2 tm => lfhas (app lf_1 lf_2) tm.
  (* of:tm -> ty -> type *)
  pi lf_1\lfhas lf_1 tm => pi lf_2\lfhas lf_2 ty => lfisty (of lf_1 lf_2).
  (* of/u:of u i *)
  lfhas of/u (of u i).
  (* of/app:
       ({A:ty} {B:ty} {M:tm} {N:tm} of M (arr A B) -> of N A ->
          of (app M N) B) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi M\lfhas M tm =>
        pi N\lfhas N tm =>
          pi lf_1\lfhas lf_1 (of M (arr A B)) =>
            pi lf_2\lfhas lf_2 (of N A) =>
              lfhas (of/app A B M N lf_1 lf_2) (of (app M N) B).
  (* of/lam:
       ({A:ty} {B:ty} {R:tm -> tm} ({x:tm} of x A -> of (R x) B) ->
          of (lam A ([x] R x)) (arr A B)) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi R\(pi lf_1\lfhas lf_1 tm => lfhas (R lf_1) tm) =>
        pi lf_1\(pi x\lfhas x tm =>
                   pi lf_2\lfhas lf_2 (of x A) =>
                     lfhas (lf_1 x lf_2) (of (R x) B)) =>
          lfhas (of/lam A B R lf_1) (of (lam A (x\R x)) (arr A B)).
end.

Abella < Define ctx : olist -> prop by 
ctx nil;
nabla x p, ctx (<p:of x A> :: <x:tm> :: G) := ctx G.

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

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

member_prune < induction on 1.

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

member_prune < intros.

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

member_prune < case H1.

Subgoal 1:

Variables: G2 G1
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
============================
 exists F, z1\G1 = x\F

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

member_prune < search.

Subgoal 2:

Variables: E G2 G1
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
H2 : member (E n1) G2 *
============================
 exists F, E = x\F

member_prune < apply IH to H2.

Subgoal 2:

Variables: G2 G1 F
IH : forall G E, (nabla n, member (E n) G * -> (exists F, E = x\F))
H2 : member F G2 *
============================
 exists F1, z1\F = x\F1

member_prune < search.
Proof completed.

Abella < Define fresh : lfobj -> lfobj -> prop by 
nabla x, fresh x A.

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

Abella < Theorem ctx_mem : 
forall G E, ctx G -> member E G -> (exists X, E = <X:tm> /\ name X) \/
  (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A).

============================
 forall G E, ctx G -> member E G -> (exists X, E = <X:tm> /\ name X) \/
   (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < induction on 1.

IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 forall G E, ctx G @ -> member E G -> (exists X, E = <X:tm> /\ name X) \/
   (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < intros.

Variables: G E
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H1 : ctx G @
H2 : member E G
============================
 (exists X, E = <X:tm> /\ name X) \/
   (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < case H1.

Subgoal 1:

Variables: E
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H2 : member E nil
============================
 (exists X, E = <X:tm> /\ name X) \/
   (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)

Subgoal 2 is:
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < case H2.

Subgoal 2:

Variables: E G1 A
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H2 : member (E n1 n2) (<n2:of n1 A> :: <n1:tm> :: G1)
H3 : ctx G1 *
============================
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < case H2.

Subgoal 2.1:

Variables: G1 A
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
============================
 (exists X, <n2:of n1 A> = <X:tm> /\ name X) \/
   (exists P X A1, <n2:of n1 A> = <P:of X A1> /\ fresh X A1 /\ fresh P A1)

Subgoal 2.2 is:
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < search.

Subgoal 2.2:

Variables: E G1 A
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
H4 : member (E n1 n2) (<n1:tm> :: G1)
============================
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < case H4.

Subgoal 2.2.1:

Variables: G1 A
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
============================
 (exists X, <n1:tm> = <X:tm> /\ name X) \/
   (exists P X A, <n1:tm> = <P:of X A> /\ fresh X A /\ fresh P A)

Subgoal 2.2.2 is:
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < search.

Subgoal 2.2.2:

Variables: E G1 A
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
H5 : member (E n1 n2) G1
============================
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < apply IH to H3 H5.

Subgoal 2.2.2:

Variables: E G1 A
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
H5 : member (E n1 n2) G1
H6 : (exists X, E n1 n2 = <X:tm> /\ name X) \/
       (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 (exists X, E n1 n2 = <X:tm> /\ name X) \/
   (exists P X A, E n1 n2 = <P:of X A> /\ fresh X A /\ fresh P A)

ctx_mem < case H6.

Subgoal 2.2.2.1:

Variables: G1 A X
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
H5 : member <X n2 n1:tm> G1
H7 : name (X n2 n1)
============================
 (exists X1, <X n2 n1:tm> = <X1:tm> /\ name X1) \/
   (exists P X1 A, <X n2 n1:tm> = <P:of X1 A> /\ fresh X1 A /\ fresh P A)

Subgoal 2.2.2.2 is:
 (exists X1, <P n2 n1:of (X n2 n1) (A1 n2 n1)> = <X1:tm> /\ name X1) \/
   (exists P1 X1 A, <P n2 n1:of (X n2 n1) (A1 n2 n1)> = <P1:of X1 A> /\
      fresh X1 A /\ fresh P1 A)

ctx_mem < search.

Subgoal 2.2.2.2:

Variables: G1 A P X A1
IH : forall G E, ctx G * -> member E G -> (exists X, E = <X:tm> /\ name X) \/
       (exists P X A, E = <P:of X A> /\ fresh X A /\ fresh P A)
H3 : ctx G1 *
H5 : member <P n2 n1:of (X n2 n1) (A1 n2 n1)> G1
H7 : fresh (X n2 n1) (A1 n2 n1)
H8 : fresh (P n2 n1) (A1 n2 n1)
============================
 (exists X1, <P n2 n1:of (X n2 n1) (A1 n2 n1)> = <X1:tm> /\ name X1) \/
   (exists P1 X1 A, <P n2 n1:of (X n2 n1) (A1 n2 n1)> = <P1:of X1 A> /\
      fresh X1 A /\ fresh P1 A)

ctx_mem < search.
Proof completed.

Abella < Theorem ctx_unique : 
forall G P Q X A B, ctx G -> member <P:of X A> G -> member <Q:of X B> G ->
  A = B /\ P = Q.

============================
 forall G P Q X A B, ctx G -> member <P:of X A> G -> member <Q:of X B> G ->
   A = B /\ P = Q

ctx_unique < induction on 1.

IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
============================
 forall G P Q X A B, ctx G @ -> member <P:of X A> G -> member <Q:of X B> G ->
   A = B /\ P = Q

ctx_unique < intros.

Variables: G P Q X A B
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H1 : ctx G @
H2 : member <P:of X A> G
H3 : member <Q:of X B> G
============================
 A = B /\ P = Q

ctx_unique < case H1.

Subgoal 1:

Variables: P Q X A B
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H2 : member <P:of X A> nil
H3 : member <Q:of X B> nil
============================
 A = B /\ P = Q

Subgoal 2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H2.

Subgoal 2:

Variables: P Q X A B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H2 : member <P n1 n2:of (X n1 n2) (A n1 n2)> (<n2:of n1 A1> :: <n1:tm> :: G1)
H3 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> (<n2:of n1 A1> :: <n1:tm> :: G1)
H4 : ctx G1 *
============================
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H2.

Subgoal 2.1:

Variables: Q B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H3 : member <Q n1 n2:of n1 (B n1 n2)> (<n2:of n1 A1> :: <n1:tm> :: G1)
H4 : ctx G1 *
============================
 A1 = B n1 n2 /\ n2 = Q n1 n2

Subgoal 2.2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H3.

Subgoal 2.1.1:

Variables: G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
============================
 A1 = A1 /\ n2 = n2

Subgoal 2.1.2 is:
 A1 = B n1 n2 /\ n2 = Q n1 n2

Subgoal 2.2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < search.

Subgoal 2.1.2:

Variables: Q B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H5 : member <Q n1 n2:of n1 (B n1 n2)> (<n1:tm> :: G1)
============================
 A1 = B n1 n2 /\ n2 = Q n1 n2

Subgoal 2.2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H5.

Subgoal 2.1.2:

Variables: Q B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H6 : member <Q n1 n2:of n1 (B n1 n2)> G1
============================
 A1 = B n1 n2 /\ n2 = Q n1 n2

Subgoal 2.2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < apply member_prune to H6.

Subgoal 2.2:

Variables: P Q X A B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H3 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> (<n2:of n1 A1> :: <n1:tm> :: G1)
H4 : ctx G1 *
H5 : member <P n1 n2:of (X n1 n2) (A n1 n2)> (<n1:tm> :: G1)
============================
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H3.

Subgoal 2.2.1:

Variables: P A G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H5 : member <P n1 n2:of n1 (A n1 n2)> (<n1:tm> :: G1)
============================
 A n1 n2 = A1 /\ P n1 n2 = n2

Subgoal 2.2.2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H5.

Subgoal 2.2.1:

Variables: P A G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H6 : member <P n1 n2:of n1 (A n1 n2)> G1
============================
 A n1 n2 = A1 /\ P n1 n2 = n2

Subgoal 2.2.2 is:
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < apply member_prune to H6.

Subgoal 2.2.2:

Variables: P Q X A B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H5 : member <P n1 n2:of (X n1 n2) (A n1 n2)> (<n1:tm> :: G1)
H6 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> (<n1:tm> :: G1)
============================
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H5.

Subgoal 2.2.2:

Variables: P Q X A B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H6 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> (<n1:tm> :: G1)
H7 : member <P n1 n2:of (X n1 n2) (A n1 n2)> G1
============================
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < case H6.

Subgoal 2.2.2:

Variables: P Q X A B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H7 : member <P n1 n2:of (X n1 n2) (A n1 n2)> G1
H8 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> G1
============================
 A n1 n2 = B n1 n2 /\ P n1 n2 = Q n1 n2

ctx_unique < apply IH to H4 H7 H8.

Subgoal 2.2.2:

Variables: Q X B G1 A1
IH : forall G P Q X A B, ctx G * -> member <P:of X A> G ->
       member <Q:of X B> G -> A = B /\ P = Q
H4 : ctx G1 *
H7 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> G1
H8 : member <Q n1 n2:of (X n1 n2) (B n1 n2)> G1
============================
 B n1 n2 = B n1 n2 /\ Q n1 n2 = Q n1 n2

ctx_unique < search.
Proof completed.

Abella < Theorem unique_ty : 
forall G M A B P1 P2, ctx G -> <G |- P1:of M A> -> <G |- P2:of M B> -> A = B.

============================
 forall G M A B P1 P2, ctx G -> <G |- P1:of M A> -> <G |- P2:of M B> -> A = B

unique_ty < induction on 2.

IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
============================
 forall G M A B P1 P2, ctx G -> <G |- P1:of M A>@ -> <G |- P2:of M B> -> A =
   B

unique_ty < intros.

Variables: G M A B P1 P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H2 : <G |- P1:of M A>@
H3 : <G |- P2:of M B>
============================
 A = B

unique_ty < case H2.

Subgoal 1:

Variables: G B P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of u B>
============================
 i = B

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H3.

Subgoal 1.1:

Variables: G
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
============================
 i = i

Subgoal 1.2 is:
 i = B

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < search.

Subgoal 1.2:

Variables: G B P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [F] |- P2:of u B>
H5 : member F G
============================
 i = B

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < apply ctx_mem to H1 H5.

Subgoal 1.2:

Variables: G B P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [F] |- P2:of u B>
H5 : member F G
H6 : (exists X, F = <X:tm> /\ name X) \/
       (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 i = B

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H6.

Subgoal 1.2.1:

Variables: G B P2 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [X:tm] |- P2:of u B>
H5 : member <X:tm> G
H7 : name X
============================
 i = B

Subgoal 1.2.2 is:
 i = B

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H4.

Subgoal 1.2.2:

Variables: G B P2 P X A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P2:of u B>
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
============================
 i = B

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H7.

Subgoal 1.2.2:

Variables: G B P2 P A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx (G n1)
H4 : <G n1, [P n1:of n1 A2] |- P2 n1:of u (B n1)>
H5 : member <P n1:of n1 A2> (G n1)
H8 : fresh (P n1) A2
============================
 i = B n1

Subgoal 2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H4.

Subgoal 2:

Variables: G A B P2 A1 N lf_2 M1 lf_1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of (app M1 N) B>
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
============================
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H3.

Subgoal 2.1:

Variables: G A B A1 N lf_2 M1 lf_1 A2 lf_4 lf_3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G |- A2:ty>
H11 : <G |- B:ty>
H12 : <G |- M1:tm>
H13 : <G |- N:tm>
H14 : <G |- lf_3:of M1 (arr A2 B)>
H15 : <G |- lf_4:of N A2>
============================
 A = B

Subgoal 2.2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < apply IH to H1 H8 H14.

Subgoal 2.1:

Variables: G B N lf_2 M1 lf_1 A2 lf_4 lf_3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A2:ty>*
H5 : <G |- B:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A2 B)>*
H9 : <G |- lf_2:of N A2>*
H10 : <G |- A2:ty>
H11 : <G |- B:ty>
H12 : <G |- M1:tm>
H13 : <G |- N:tm>
H14 : <G |- lf_3:of M1 (arr A2 B)>
H15 : <G |- lf_4:of N A2>
============================
 B = B

Subgoal 2.2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < search.

Subgoal 2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [F] |- P2:of (app M1 N) B>
H11 : member F G
============================
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < apply ctx_mem to H1 H11.

Subgoal 2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [F] |- P2:of (app M1 N) B>
H11 : member F G
H12 : (exists X, F = <X:tm> /\ name X) \/
        (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H12.

Subgoal 2.2.1:

Variables: G A B P2 A1 N lf_2 M1 lf_1 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [X:tm] |- P2:of (app M1 N) B>
H11 : member <X:tm> G
H13 : name X
============================
 A = B

Subgoal 2.2.2 is:
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H10.

Subgoal 2.2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 P X A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [P:of X A2] |- P2:of (app M1 N) B>
H11 : member <P:of X A2> G
H13 : fresh X A2
H14 : fresh P A2
============================
 A = B

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H13.

Subgoal 2.2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 P A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx (G n1)
H4 : <G n1 |- A1 n1:ty>*
H5 : <G n1 |- A n1:ty>*
H6 : <G n1 |- M1 n1:tm>*
H7 : <G n1 |- N n1:tm>*
H8 : <G n1 |- lf_1 n1:of (M1 n1) (arr (A1 n1) (A n1))>*
H9 : <G n1 |- lf_2 n1:of (N n1) (A1 n1)>*
H10 : <G n1, [P n1:of n1 A3] |- P2 n1:of (app (M1 n1) (N n1)) (B n1)>
H11 : member <P n1:of n1 A3> (G n1)
H14 : fresh (P n1) A3
============================
 A n1 = B n1

Subgoal 3 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H10.

Subgoal 3:

Variables: G B P2 B1 R lf_1 A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of (lam A1 ([x] R x)) B>
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
============================
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H3.

Subgoal 3.1:

Variables: G B1 R lf_1 A1 B2 lf_2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G |- A1:ty>
H9 : <G |- B2:ty>
H10 : <G, n1:tm |- R n1:tm>
H11 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B2>
============================
 arr A1 B1 = arr A1 B2

Subgoal 3.2 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < apply IH to _ H7 H11.

Subgoal 3.1:

Variables: G R lf_1 A1 B2 lf_2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B2:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B2>*
H8 : <G |- A1:ty>
H9 : <G |- B2:ty>
H10 : <G, n1:tm |- R n1:tm>
H11 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B2>
============================
 arr A1 B2 = arr A1 B2

Subgoal 3.2 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < search.

Subgoal 3.2:

Variables: G B P2 B1 R lf_1 A1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [F] |- P2:of (lam A1 ([x] R x)) B>
H9 : member F G
============================
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < apply ctx_mem to H1 H9.

Subgoal 3.2:

Variables: G B P2 B1 R lf_1 A1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [F] |- P2:of (lam A1 ([x] R x)) B>
H9 : member F G
H10 : (exists X, F = <X:tm> /\ name X) \/
        (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H10.

Subgoal 3.2.1:

Variables: G B P2 B1 R lf_1 A1 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [X:tm] |- P2:of (lam A1 ([x] R x)) B>
H9 : member <X:tm> G
H11 : name X
============================
 arr A1 B1 = B

Subgoal 3.2.2 is:
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H8.

Subgoal 3.2.2:

Variables: G B P2 B1 R lf_1 A1 P X A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [P:of X A2] |- P2:of (lam A1 ([x] R x)) B>
H9 : member <P:of X A2> G
H11 : fresh X A2
H12 : fresh P A2
============================
 arr A1 B1 = B

Subgoal 4 is:
 A = B

unique_ty < case H11.

Subgoal 3.2.2:

Variables: G B P2 B1 R lf_1 A1 P A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx (G n3)
H4 : <G n3 |- A1 n3:ty>*
H5 : <G n3 |- B1 n3:ty>*
H6 : <G n3, n1:tm |- R n3 n1:tm>*
H7 : <G n3, n1:tm, n2:of n1 (A1 n3) |- lf_1 n3 n1 n2:of (R n3 n1) (B1 n3)>*
H8 : <G n3, [P n3:of n3 A3] |- P2 n3:of (lam (A1 n3) ([x] R n3 x)) (B n3)>
H9 : member <P n3:of n3 A3> (G n3)
H12 : fresh (P n3) A3
============================
 arr (A1 n3) (B1 n3) = B n3

Subgoal 4 is:
 A = B

unique_ty < case H8.

Subgoal 4:

Variables: G M A B P1 P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [F] |- P1:of M A>*
H5 : member F G
============================
 A = B

unique_ty < apply ctx_mem to H1 H5.

Subgoal 4:

Variables: G M A B P1 P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [F] |- P1:of M A>*
H5 : member F G
H6 : (exists X, F = <X:tm> /\ name X) \/
       (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 A = B

unique_ty < case H6.

Subgoal 4.1:

Variables: G M A B P1 P2 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [X:tm] |- P1:of M A>*
H5 : member <X:tm> G
H7 : name X
============================
 A = B

Subgoal 4.2 is:
 A = B

unique_ty < case H4.

Subgoal 4.2:

Variables: G M A B P1 P2 P X A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
============================
 A = B

unique_ty < case H3.

Subgoal 4.2.1:

Variables: G A P1 P X A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of u A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
============================
 A = i

Subgoal 4.2.2 is:
 A = B

Subgoal 4.2.3 is:
 A = arr A2 B1

Subgoal 4.2.4 is:
 A = B

unique_ty < case H7.

Subgoal 4.2.1:

Variables: G A P1 P A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx (G n1)
H4 : <G n1, [P n1:of n1 A2] |- P1 n1:of u (A n1)>*
H5 : member <P n1:of n1 A2> (G n1)
H8 : fresh (P n1) A2
============================
 A n1 = i

Subgoal 4.2.2 is:
 A = B

Subgoal 4.2.3 is:
 A = arr A2 B1

Subgoal 4.2.4 is:
 A = B

unique_ty < case H4.

Subgoal 4.2.2:

Variables: G A B P1 P X A1 A2 N lf_2 M1 lf_1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of (app M1 N) A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G |- A2:ty>
H10 : <G |- B:ty>
H11 : <G |- M1:tm>
H12 : <G |- N:tm>
H13 : <G |- lf_1:of M1 (arr A2 B)>
H14 : <G |- lf_2:of N A2>
============================
 A = B

Subgoal 4.2.3 is:
 A = arr A2 B1

Subgoal 4.2.4 is:
 A = B

unique_ty < case H7.

Subgoal 4.2.2:

Variables: G A B P1 P A2 N lf_2 M1 lf_1 A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx (G n1)
H4 : <G n1, [P n1:of n1 A3] |- P1 n1:of (app (M1 n1) (N n1)) (A n1)>*
H5 : member <P n1:of n1 A3> (G n1)
H8 : fresh (P n1) A3
H9 : <G n1 |- A2 n1:ty>
H10 : <G n1 |- B n1:ty>
H11 : <G n1 |- M1 n1:tm>
H12 : <G n1 |- N n1:tm>
H13 : <G n1 |- lf_1 n1:of (M1 n1) (arr (A2 n1) (B n1))>
H14 : <G n1 |- lf_2 n1:of (N n1) (A2 n1)>
============================
 A n1 = B n1

Subgoal 4.2.3 is:
 A = arr A2 B1

Subgoal 4.2.4 is:
 A = B

unique_ty < case H4.

Subgoal 4.2.3:

Variables: G A P1 P X A1 B1 R lf_1 A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of (lam A2 ([x] R x)) A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G |- A2:ty>
H10 : <G |- B1:ty>
H11 : <G, n1:tm |- R n1:tm>
H12 : <G, n1:tm, n2:of n1 A2 |- lf_1 n1 n2:of (R n1) B1>
============================
 A = arr A2 B1

Subgoal 4.2.4 is:
 A = B

unique_ty < case H7.

Subgoal 4.2.3:

Variables: G A P1 P B1 R lf_1 A2 A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx (G n3)
H4 : <G n3, [P n3:of n3 A3] |- P1 n3:of (lam (A2 n3) ([x] R n3 x)) (A n3)>*
H5 : member <P n3:of n3 A3> (G n3)
H8 : fresh (P n3) A3
H9 : <G n3 |- A2 n3:ty>
H10 : <G n3 |- B1 n3:ty>
H11 : <G n3, n1:tm |- R n3 n1:tm>
H12 : <G n3, n1:tm, n2:of n1 (A2 n3) |- lf_1 n3 n1 n2:of (R n3 n1) (B1 n3)>
============================
 A n3 = arr (A2 n3) (B1 n3)

Subgoal 4.2.4 is:
 A = B

unique_ty < case H4.

Subgoal 4.2.4:

Variables: G M A B P1 P2 P X A1 F1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [F1] |- P2:of M B>
H10 : member F1 G
============================
 A = B

unique_ty < apply ctx_mem to H1 H10.

Subgoal 4.2.4:

Variables: G M A B P1 P2 P X A1 F1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [F1] |- P2:of M B>
H10 : member F1 G
H11 : (exists X, F1 = <X:tm> /\ name X) \/
        (exists P X A, F1 = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 A = B

unique_ty < case H11.

Subgoal 4.2.4.1:

Variables: G M A B P1 P2 P X A1 X1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [X1:tm] |- P2:of M B>
H10 : member <X1:tm> G
H12 : name X1
============================
 A = B

Subgoal 4.2.4.2 is:
 A = B

unique_ty < case H9.

Subgoal 4.2.4.2:

Variables: G M A B P1 P2 P X A1 P3 X1 A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [P3:of X1 A2] |- P2:of M B>
H10 : member <P3:of X1 A2> G
H12 : fresh X1 A2
H13 : fresh P3 A2
============================
 A = B

unique_ty < case H4.

Subgoal 4.2.4.2:

Variables: G M A B P1 P2 P3 X1 A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H5 : member <P1:of M A> G
H7 : fresh M A
H8 : fresh P1 A
H9 : <G, [P3:of X1 A2] |- P2:of M B>
H10 : member <P3:of X1 A2> G
H12 : fresh X1 A2
H13 : fresh P3 A2
============================
 A = B

unique_ty < case H9.

Subgoal 4.2.4.2:

Variables: G M A B P1 P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H5 : member <P1:of M A> G
H7 : fresh M A
H8 : fresh P1 A
H10 : member <P2:of M B> G
H12 : fresh M B
H13 : fresh P2 B
============================
 A = B

unique_ty < apply ctx_unique to H1 H5 H10.

Subgoal 4.2.4.2:

Variables: G M B P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       A = B
H1 : ctx G
H5 : member <P2:of M B> G
H7 : fresh M B
H8 : fresh P2 B
H10 : member <P2:of M B> G
H12 : fresh M B
H13 : fresh P2 B
============================
 B = B

unique_ty < search.
Proof completed.

Abella < Theorem unique_proof : 
forall G M A B P1 P2, ctx G -> <G |- P1:of M A> -> <G |- P2:of M B> -> P1 =
  P2.

============================
 forall G M A B P1 P2, ctx G -> <G |- P1:of M A> -> <G |- P2:of M B> -> P1 =
   P2

unique_proof < induction on 2.

IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
============================
 forall G M A B P1 P2, ctx G -> <G |- P1:of M A>@ -> <G |- P2:of M B> -> P1 =
   P2

unique_proof < intros.

Variables: G M A B P1 P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H2 : <G |- P1:of M A>@
H3 : <G |- P2:of M B>
============================
 P1 = P2

unique_proof < case H2.

Subgoal 1:

Variables: G B P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of u B>
============================
 of/u = P2

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H3.

Subgoal 1.1:

Variables: G
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
============================
 of/u = of/u

Subgoal 1.2 is:
 of/u = P2

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < search.

Subgoal 1.2:

Variables: G B P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [F] |- P2:of u B>
H5 : member F G
============================
 of/u = P2

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply ctx_mem to H1 H5.

Subgoal 1.2:

Variables: G B P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [F] |- P2:of u B>
H5 : member F G
H6 : (exists X, F = <X:tm> /\ name X) \/
       (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 of/u = P2

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H6.

Subgoal 1.2.1:

Variables: G B P2 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [X:tm] |- P2:of u B>
H5 : member <X:tm> G
H7 : name X
============================
 of/u = P2

Subgoal 1.2.2 is:
 of/u = P2

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H4.

Subgoal 1.2.2:

Variables: G B P2 P X A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P2:of u B>
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
============================
 of/u = P2

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H7.

Subgoal 1.2.2:

Variables: G B P2 P A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx (G n1)
H4 : <G n1, [P n1:of n1 A2] |- P2 n1:of u (B n1)>
H5 : member <P n1:of n1 A2> (G n1)
H8 : fresh (P n1) A2
============================
 of/u = P2 n1

Subgoal 2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H4.

Subgoal 2:

Variables: G A B P2 A1 N lf_2 M1 lf_1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of (app M1 N) B>
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
============================
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H3.

Subgoal 2.1:

Variables: G A B A1 N lf_2 M1 lf_1 A2 lf_4 lf_3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G |- A2:ty>
H11 : <G |- B:ty>
H12 : <G |- M1:tm>
H13 : <G |- N:tm>
H14 : <G |- lf_3:of M1 (arr A2 B)>
H15 : <G |- lf_4:of N A2>
============================
 of/app A1 A M1 N lf_1 lf_2 = of/app A2 B M1 N lf_3 lf_4

Subgoal 2.2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply IH to H1 H8 H14.

Subgoal 2.1:

Variables: G A B A1 N lf_2 M1 A2 lf_4 lf_3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_3:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G |- A2:ty>
H11 : <G |- B:ty>
H12 : <G |- M1:tm>
H13 : <G |- N:tm>
H14 : <G |- lf_3:of M1 (arr A2 B)>
H15 : <G |- lf_4:of N A2>
============================
 of/app A1 A M1 N lf_3 lf_2 = of/app A2 B M1 N lf_3 lf_4

Subgoal 2.2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply IH to H1 H9 H15.

Subgoal 2.1:

Variables: G A B A1 N M1 A2 lf_4 lf_3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_3:of M1 (arr A1 A)>*
H9 : <G |- lf_4:of N A1>*
H10 : <G |- A2:ty>
H11 : <G |- B:ty>
H12 : <G |- M1:tm>
H13 : <G |- N:tm>
H14 : <G |- lf_3:of M1 (arr A2 B)>
H15 : <G |- lf_4:of N A2>
============================
 of/app A1 A M1 N lf_3 lf_4 = of/app A2 B M1 N lf_3 lf_4

Subgoal 2.2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply unique_ty to H1 H8 H14.

Subgoal 2.1:

Variables: G B N M1 A2 lf_4 lf_3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A2:ty>*
H5 : <G |- B:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_3:of M1 (arr A2 B)>*
H9 : <G |- lf_4:of N A2>*
H10 : <G |- A2:ty>
H11 : <G |- B:ty>
H12 : <G |- M1:tm>
H13 : <G |- N:tm>
H14 : <G |- lf_3:of M1 (arr A2 B)>
H15 : <G |- lf_4:of N A2>
============================
 of/app A2 B M1 N lf_3 lf_4 = of/app A2 B M1 N lf_3 lf_4

Subgoal 2.2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < search.

Subgoal 2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [F] |- P2:of (app M1 N) B>
H11 : member F G
============================
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply ctx_mem to H1 H11.

Subgoal 2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [F] |- P2:of (app M1 N) B>
H11 : member F G
H12 : (exists X, F = <X:tm> /\ name X) \/
        (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H12.

Subgoal 2.2.1:

Variables: G A B P2 A1 N lf_2 M1 lf_1 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [X:tm] |- P2:of (app M1 N) B>
H11 : member <X:tm> G
H13 : name X
============================
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 2.2.2 is:
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H10.

Subgoal 2.2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 P X A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- A:ty>*
H6 : <G |- M1:tm>*
H7 : <G |- N:tm>*
H8 : <G |- lf_1:of M1 (arr A1 A)>*
H9 : <G |- lf_2:of N A1>*
H10 : <G, [P:of X A2] |- P2:of (app M1 N) B>
H11 : member <P:of X A2> G
H13 : fresh X A2
H14 : fresh P A2
============================
 of/app A1 A M1 N lf_1 lf_2 = P2

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H13.

Subgoal 2.2.2:

Variables: G A B P2 A1 N lf_2 M1 lf_1 P A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx (G n1)
H4 : <G n1 |- A1 n1:ty>*
H5 : <G n1 |- A n1:ty>*
H6 : <G n1 |- M1 n1:tm>*
H7 : <G n1 |- N n1:tm>*
H8 : <G n1 |- lf_1 n1:of (M1 n1) (arr (A1 n1) (A n1))>*
H9 : <G n1 |- lf_2 n1:of (N n1) (A1 n1)>*
H10 : <G n1, [P n1:of n1 A3] |- P2 n1:of (app (M1 n1) (N n1)) (B n1)>
H11 : member <P n1:of n1 A3> (G n1)
H14 : fresh (P n1) A3
============================
 of/app (A1 n1) (A n1) (M1 n1) (N n1) (lf_1 n1) (lf_2 n1) = P2 n1

Subgoal 3 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H10.

Subgoal 3:

Variables: G B P2 B1 R lf_1 A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of (lam A1 ([x] R x)) B>
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
============================
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H3.

Subgoal 3.1:

Variables: G B1 R lf_1 A1 B2 lf_2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G |- A1:ty>
H9 : <G |- B2:ty>
H10 : <G, n1:tm |- R n1:tm>
H11 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B2>
============================
 of/lam A1 B1 R lf_1 = of/lam A1 B2 (z1\R z1) lf_2

Subgoal 3.2 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply IH to _ H7 H11.

Subgoal 3.1:

Variables: G B1 R A1 B2 lf_2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B1>*
H8 : <G |- A1:ty>
H9 : <G |- B2:ty>
H10 : <G, n1:tm |- R n1:tm>
H11 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B2>
============================
 of/lam A1 B1 R (z1\z2\lf_2 z1 z2) = of/lam A1 B2 (z1\R z1) lf_2

Subgoal 3.2 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply unique_ty to _ H7 H11.

Subgoal 3.1:

Variables: G R A1 B2 lf_2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B2:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B2>*
H8 : <G |- A1:ty>
H9 : <G |- B2:ty>
H10 : <G, n1:tm |- R n1:tm>
H11 : <G, n1:tm, n2:of n1 A1 |- lf_2 n1 n2:of (R n1) B2>
============================
 of/lam A1 B2 R (z1\z2\lf_2 z1 z2) = of/lam A1 B2 (z1\R z1) lf_2

Subgoal 3.2 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < search.

Subgoal 3.2:

Variables: G B P2 B1 R lf_1 A1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [F] |- P2:of (lam A1 ([x] R x)) B>
H9 : member F G
============================
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < apply ctx_mem to H1 H9.

Subgoal 3.2:

Variables: G B P2 B1 R lf_1 A1 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [F] |- P2:of (lam A1 ([x] R x)) B>
H9 : member F G
H10 : (exists X, F = <X:tm> /\ name X) \/
        (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H10.

Subgoal 3.2.1:

Variables: G B P2 B1 R lf_1 A1 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [X:tm] |- P2:of (lam A1 ([x] R x)) B>
H9 : member <X:tm> G
H11 : name X
============================
 of/lam A1 B1 R lf_1 = P2

Subgoal 3.2.2 is:
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H8.

Subgoal 3.2.2:

Variables: G B P2 B1 R lf_1 A1 P X A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G |- A1:ty>*
H5 : <G |- B1:ty>*
H6 : <G, n1:tm |- R n1:tm>*
H7 : <G, n1:tm, n2:of n1 A1 |- lf_1 n1 n2:of (R n1) B1>*
H8 : <G, [P:of X A2] |- P2:of (lam A1 ([x] R x)) B>
H9 : member <P:of X A2> G
H11 : fresh X A2
H12 : fresh P A2
============================
 of/lam A1 B1 R lf_1 = P2

Subgoal 4 is:
 P1 = P2

unique_proof < case H11.

Subgoal 3.2.2:

Variables: G B P2 B1 R lf_1 A1 P A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx (G n3)
H4 : <G n3 |- A1 n3:ty>*
H5 : <G n3 |- B1 n3:ty>*
H6 : <G n3, n1:tm |- R n3 n1:tm>*
H7 : <G n3, n1:tm, n2:of n1 (A1 n3) |- lf_1 n3 n1 n2:of (R n3 n1) (B1 n3)>*
H8 : <G n3, [P n3:of n3 A3] |- P2 n3:of (lam (A1 n3) ([x] R n3 x)) (B n3)>
H9 : member <P n3:of n3 A3> (G n3)
H12 : fresh (P n3) A3
============================
 of/lam (A1 n3) (B1 n3) (R n3) (lf_1 n3) = P2 n3

Subgoal 4 is:
 P1 = P2

unique_proof < case H8.

Subgoal 4:

Variables: G M A B P1 P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [F] |- P1:of M A>*
H5 : member F G
============================
 P1 = P2

unique_proof < apply ctx_mem to H1 H5.

Subgoal 4:

Variables: G M A B P1 P2 F
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [F] |- P1:of M A>*
H5 : member F G
H6 : (exists X, F = <X:tm> /\ name X) \/
       (exists P X A, F = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 P1 = P2

unique_proof < case H6.

Subgoal 4.1:

Variables: G M A B P1 P2 X
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [X:tm] |- P1:of M A>*
H5 : member <X:tm> G
H7 : name X
============================
 P1 = P2

Subgoal 4.2 is:
 P1 = P2

unique_proof < case H4.

Subgoal 4.2:

Variables: G M A B P1 P2 P X A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H3 : <G |- P2:of M B>
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
============================
 P1 = P2

unique_proof < case H3.

Subgoal 4.2.1:

Variables: G A P1 P X A1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of u A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
============================
 P1 = of/u

Subgoal 4.2.2 is:
 P1 = of/app A2 B M1 N lf_1 lf_2

Subgoal 4.2.3 is:
 P1 = of/lam A2 B1 R lf_1

Subgoal 4.2.4 is:
 P1 = P2

unique_proof < case H7.

Subgoal 4.2.1:

Variables: G A P1 P A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx (G n1)
H4 : <G n1, [P n1:of n1 A2] |- P1 n1:of u (A n1)>*
H5 : member <P n1:of n1 A2> (G n1)
H8 : fresh (P n1) A2
============================
 P1 n1 = of/u

Subgoal 4.2.2 is:
 P1 = of/app A2 B M1 N lf_1 lf_2

Subgoal 4.2.3 is:
 P1 = of/lam A2 B1 R lf_1

Subgoal 4.2.4 is:
 P1 = P2

unique_proof < case H4.

Subgoal 4.2.2:

Variables: G A B P1 P X A1 A2 N lf_2 M1 lf_1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of (app M1 N) A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G |- A2:ty>
H10 : <G |- B:ty>
H11 : <G |- M1:tm>
H12 : <G |- N:tm>
H13 : <G |- lf_1:of M1 (arr A2 B)>
H14 : <G |- lf_2:of N A2>
============================
 P1 = of/app A2 B M1 N lf_1 lf_2

Subgoal 4.2.3 is:
 P1 = of/lam A2 B1 R lf_1

Subgoal 4.2.4 is:
 P1 = P2

unique_proof < case H7.

Subgoal 4.2.2:

Variables: G A B P1 P A2 N lf_2 M1 lf_1 A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx (G n1)
H4 : <G n1, [P n1:of n1 A3] |- P1 n1:of (app (M1 n1) (N n1)) (A n1)>*
H5 : member <P n1:of n1 A3> (G n1)
H8 : fresh (P n1) A3
H9 : <G n1 |- A2 n1:ty>
H10 : <G n1 |- B n1:ty>
H11 : <G n1 |- M1 n1:tm>
H12 : <G n1 |- N n1:tm>
H13 : <G n1 |- lf_1 n1:of (M1 n1) (arr (A2 n1) (B n1))>
H14 : <G n1 |- lf_2 n1:of (N n1) (A2 n1)>
============================
 P1 n1 = of/app (A2 n1) (B n1) (M1 n1) (N n1) (lf_1 n1) (lf_2 n1)

Subgoal 4.2.3 is:
 P1 = of/lam A2 B1 R lf_1

Subgoal 4.2.4 is:
 P1 = P2

unique_proof < case H4.

Subgoal 4.2.3:

Variables: G A P1 P X A1 B1 R lf_1 A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of (lam A2 ([x] R x)) A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G |- A2:ty>
H10 : <G |- B1:ty>
H11 : <G, n1:tm |- R n1:tm>
H12 : <G, n1:tm, n2:of n1 A2 |- lf_1 n1 n2:of (R n1) B1>
============================
 P1 = of/lam A2 B1 R lf_1

Subgoal 4.2.4 is:
 P1 = P2

unique_proof < case H7.

Subgoal 4.2.3:

Variables: G A P1 P B1 R lf_1 A2 A3
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx (G n3)
H4 : <G n3, [P n3:of n3 A3] |- P1 n3:of (lam (A2 n3) ([x] R n3 x)) (A n3)>*
H5 : member <P n3:of n3 A3> (G n3)
H8 : fresh (P n3) A3
H9 : <G n3 |- A2 n3:ty>
H10 : <G n3 |- B1 n3:ty>
H11 : <G n3, n1:tm |- R n3 n1:tm>
H12 : <G n3, n1:tm, n2:of n1 (A2 n3) |- lf_1 n3 n1 n2:of (R n3 n1) (B1 n3)>
============================
 P1 n3 = of/lam (A2 n3) (B1 n3) (R n3) (lf_1 n3)

Subgoal 4.2.4 is:
 P1 = P2

unique_proof < case H4.

Subgoal 4.2.4:

Variables: G M A B P1 P2 P X A1 F1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [F1] |- P2:of M B>
H10 : member F1 G
============================
 P1 = P2

unique_proof < apply ctx_mem to H1 H10.

Subgoal 4.2.4:

Variables: G M A B P1 P2 P X A1 F1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [F1] |- P2:of M B>
H10 : member F1 G
H11 : (exists X, F1 = <X:tm> /\ name X) \/
        (exists P X A, F1 = <P:of X A> /\ fresh X A /\ fresh P A)
============================
 P1 = P2

unique_proof < case H11.

Subgoal 4.2.4.1:

Variables: G M A B P1 P2 P X A1 X1
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [X1:tm] |- P2:of M B>
H10 : member <X1:tm> G
H12 : name X1
============================
 P1 = P2

Subgoal 4.2.4.2 is:
 P1 = P2

unique_proof < case H9.

Subgoal 4.2.4.2:

Variables: G M A B P1 P2 P X A1 P3 X1 A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H4 : <G, [P:of X A1] |- P1:of M A>*
H5 : member <P:of X A1> G
H7 : fresh X A1
H8 : fresh P A1
H9 : <G, [P3:of X1 A2] |- P2:of M B>
H10 : member <P3:of X1 A2> G
H12 : fresh X1 A2
H13 : fresh P3 A2
============================
 P1 = P2

unique_proof < case H4.

Subgoal 4.2.4.2:

Variables: G M A B P1 P2 P3 X1 A2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H5 : member <P1:of M A> G
H7 : fresh M A
H8 : fresh P1 A
H9 : <G, [P3:of X1 A2] |- P2:of M B>
H10 : member <P3:of X1 A2> G
H12 : fresh X1 A2
H13 : fresh P3 A2
============================
 P1 = P2

unique_proof < case H9.

Subgoal 4.2.4.2:

Variables: G M A B P1 P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H5 : member <P1:of M A> G
H7 : fresh M A
H8 : fresh P1 A
H10 : member <P2:of M B> G
H12 : fresh M B
H13 : fresh P2 B
============================
 P1 = P2

unique_proof < apply ctx_unique to H1 H5 H10.

Subgoal 4.2.4.2:

Variables: G M B P2
IH : forall G M A B P1 P2, ctx G -> <G |- P1:of M A>* -> <G |- P2:of M B> ->
       P1 = P2
H1 : ctx G
H5 : member <P2:of M B> G
H7 : fresh M B
H8 : fresh P2 B
H10 : member <P2:of M B> G
H12 : fresh M B
H13 : fresh P2 B
============================
 P2 = P2

unique_proof < search.
Proof completed.

Abella < Goodbye.