Welcome to Abella 2.0.5-dev.
Abella < Kind nat, tm, ty type.

Abella < Kind atm, atmlist type.

Abella < Type z nat.

Abella < Type s nat -> nat.

Abella < Type app tm -> tm -> tm.

Abella < Type abs (tm -> tm) -> tm.

Abella < Type arrow ty -> ty -> ty.

Abella < Type nl atmlist.

Abella < Type cons atm -> atmlist -> atmlist.

Abella < Type eval tm -> tm -> atm.

Abella < Type of tm -> ty -> atm.

Abella < Type tt o.

Abella < Type atom atm -> o.

Abella < Type or, and o -> o -> o.

Abella < Type imp atm -> o -> o.

Abella < Type all (tm -> o) -> o.

Abella < Type ex (tm -> o) -> o.

Abella < Close nat, tm, ty.

Abella < Define nat : nat -> prop by 
nat z;
nat (s N) := nat N.

Abella < Define lt : nat -> nat -> prop by 
lt z (s N);
lt (s M) (s N) := lt M N.

Abella < Define prog : atm -> o -> prop by 
prog (eval (abs R) (abs R)) tt;
prog (eval (app P Q) V) (and (atom (eval P (abs R))) (atom (eval (R Q) V)));
prog (of (abs R) (arrow A B)) (all (x\imp (of x A) (atom (of (R x) B))));
prog (of (app P Q) B) (and (atom (of P (arrow A B))) (atom (of Q A))).

Abella < Define mem : atm -> atmlist -> prop by 
mem A (cons A L);
mem A (cons B L) := mem A L.

Abella < Define seq : nat -> atmlist -> o -> prop by 
seq (s N) L tt;
seq (s N) L (atom A) := mem A L;
seq (s N) L (or A B) := seq N L A;
seq (s N) L (or A B) := seq N L B;
seq (s N) L (and A B) := seq N L A /\ seq N L B;
seq (s N) L (imp A B) := seq N (cons A L) B;
seq (s N) L (all G) := nabla x, seq N L (G x);
seq (s N) L (ex G) := exists X, seq N L (G X);
seq (s N) L (atom A) := exists B, prog A B /\ seq N L B.

Abella < Theorem seq_subset : 
forall L1 L2 G N, seq N L1 G -> (forall X, mem X L1 -> mem X L2) ->
  seq N L2 G.


============================
 forall L1 L2 G N, seq N L1 G -> (forall X, mem X L1 -> mem X L2) ->
   seq N L2 G

seq_subset < induction on 1.

IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
============================
 forall L1 L2 G N, seq N L1 G @ -> (forall X, mem X L1 -> mem X L2) ->
   seq N L2 G

seq_subset < intros.

Variables: L1 L2 G N
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H1 : seq N L1 G @
H2 : forall X, mem X L1 -> mem X L2
============================
 seq N L2 G

seq_subset < case H1.
Subgoal 1:

Variables: L1 L2 N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
============================
 seq (s N1) L2 tt

Subgoal 2 is:
 seq (s N1) L2 (atom A)

Subgoal 3 is:
 seq (s N1) L2 (or A B)

Subgoal 4 is:
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 2:

Variables: L1 L2 A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : mem A L1
============================
 seq (s N1) L2 (atom A)

Subgoal 3 is:
 seq (s N1) L2 (or A B)

Subgoal 4 is:
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply H2 to H3.
Subgoal 2:

Variables: L1 L2 A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : mem A L1
H4 : mem A L2
============================
 seq (s N1) L2 (atom A)

Subgoal 3 is:
 seq (s N1) L2 (or A B)

Subgoal 4 is:
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 3:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 A *
============================
 seq (s N1) L2 (or A B)

Subgoal 4 is:
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H3 H2.
Subgoal 3:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 A *
H4 : seq N1 L2 A
============================
 seq (s N1) L2 (or A B)

Subgoal 4 is:
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 4:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 B *
============================
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H3 H2.
Subgoal 4:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 B *
H4 : seq N1 L2 B
============================
 seq (s N1) L2 (or A B)

Subgoal 5 is:
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 5:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 A *
H4 : seq N1 L1 B *
============================
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H3 H2.
Subgoal 5:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 A *
H4 : seq N1 L1 B *
H5 : seq N1 L2 A
============================
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H4 H2.
Subgoal 5:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 A *
H4 : seq N1 L1 B *
H5 : seq N1 L2 A
H6 : seq N1 L2 B
============================
 seq (s N1) L2 (and A B)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 6:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
============================
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < assert forall X, mem X (cons A L1) -> mem X (cons A L2).
Subgoal 6.1:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
============================
 forall X, mem X (cons A L1) -> mem X (cons A L2)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < intros.
Subgoal 6.1:

Variables: L1 L2 B A N1 X
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
H4 : mem X (cons A L1)
============================
 mem X (cons A L2)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < case H4.
Subgoal 6.1.1:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
============================
 mem A (cons A L2)

Subgoal 6.1.2 is:
 mem X (cons A L2)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 6.1.2:

Variables: L1 L2 B A N1 X
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
H5 : mem X L1
============================
 mem X (cons A L2)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply H2 to H5.
Subgoal 6.1.2:

Variables: L1 L2 B A N1 X
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
H5 : mem X L1
H6 : mem X L2
============================
 mem X (cons A L2)

Subgoal 6 is:
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 6:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
H4 : forall X, mem X (cons A L1) -> mem X (cons A L2)
============================
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H3 H4.
Subgoal 6:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 (cons A L1) B *
H4 : forall X, mem X (cons A L1) -> mem X (cons A L2)
H5 : seq N1 (cons A L2) B
============================
 seq (s N1) L2 (imp A B)

Subgoal 7 is:
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 7:

Variables: L1 L2 G1 N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 (G1 n1) *
============================
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H3 H2.
Subgoal 7:

Variables: L1 L2 G1 N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 (G1 n1) *
H4 : seq N1 L2 (G1 n1)
============================
 seq (s N1) L2 (all G1)

Subgoal 8 is:
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 8:

Variables: L1 L2 X G1 N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 (G1 X) *
============================
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H3 H2.
Subgoal 8:

Variables: L1 L2 X G1 N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : seq N1 L1 (G1 X) *
H4 : seq N1 L2 (G1 X)
============================
 seq (s N1) L2 (ex G1)

Subgoal 9 is:
 seq (s N1) L2 (atom A)

seq_subset < search.
Subgoal 9:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : prog A B
H4 : seq N1 L1 B *
============================
 seq (s N1) L2 (atom A)

seq_subset < apply IH to H4 H2.
Subgoal 9:

Variables: L1 L2 B A N1
IH : forall L1 L2 G N, seq N L1 G * -> (forall X, mem X L1 -> mem X L2) ->
       seq N L2 G
H2 : forall X, mem X L1 -> mem X L2
H3 : prog A B
H4 : seq N1 L1 B *
H5 : seq N1 L2 B
============================
 seq (s N1) L2 (atom A)

seq_subset < search.
Proof completed.
Abella < Theorem seq_lt : 
forall L G N M, lt M N -> seq M L G -> seq N L G.


============================
 forall L G N M, lt M N -> seq M L G -> seq N L G

seq_lt < induction on 1.

IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
============================
 forall L G N M, lt M N @ -> seq M L G -> seq N L G

seq_lt < intros.

Variables: L G N M
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H1 : lt M N @
H2 : seq M L G
============================
 seq N L G

seq_lt < case H1.
Subgoal 1:

Variables: L G N1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H2 : seq z L G
============================
 seq (s N1) L G

Subgoal 2 is:
 seq (s N1) L G

seq_lt < case H2.
Subgoal 2:

Variables: L G N1 M1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H2 : seq (s M1) L G
H3 : lt M1 N1 *
============================
 seq (s N1) L G

seq_lt < case H2.
Subgoal 2.1:

Variables: L N1 M1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
============================
 seq (s N1) L tt

Subgoal 2.2 is:
 seq (s N1) L (atom A)

Subgoal 2.3 is:
 seq (s N1) L (or A B)

Subgoal 2.4 is:
 seq (s N1) L (or A B)

Subgoal 2.5 is:
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.2:

Variables: L N1 M1 A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : mem A L
============================
 seq (s N1) L (atom A)

Subgoal 2.3 is:
 seq (s N1) L (or A B)

Subgoal 2.4 is:
 seq (s N1) L (or A B)

Subgoal 2.5 is:
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.3:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L A
============================
 seq (s N1) L (or A B)

Subgoal 2.4 is:
 seq (s N1) L (or A B)

Subgoal 2.5 is:
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H4.
Subgoal 2.3:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L A
H5 : seq N1 L A
============================
 seq (s N1) L (or A B)

Subgoal 2.4 is:
 seq (s N1) L (or A B)

Subgoal 2.5 is:
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.4:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L B
============================
 seq (s N1) L (or A B)

Subgoal 2.5 is:
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H4.
Subgoal 2.4:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L B
H5 : seq N1 L B
============================
 seq (s N1) L (or A B)

Subgoal 2.5 is:
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.5:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L A
H5 : seq M1 L B
============================
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H4.
Subgoal 2.5:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L A
H5 : seq M1 L B
H6 : seq N1 L A
============================
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H5.
Subgoal 2.5:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L A
H5 : seq M1 L B
H6 : seq N1 L A
H7 : seq N1 L B
============================
 seq (s N1) L (and A B)

Subgoal 2.6 is:
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.6:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 (cons A L) B
============================
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H4.
Subgoal 2.6:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 (cons A L) B
H5 : seq N1 (cons A L) B
============================
 seq (s N1) L (imp A B)

Subgoal 2.7 is:
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.7:

Variables: L N1 M1 G1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L (G1 n1)
============================
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H4.
Subgoal 2.7:

Variables: L N1 M1 G1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L (G1 n1)
H5 : seq N1 L (G1 n1)
============================
 seq (s N1) L (all G1)

Subgoal 2.8 is:
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.8:

Variables: L N1 M1 X G1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L (G1 X)
============================
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H4.
Subgoal 2.8:

Variables: L N1 M1 X G1
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : seq M1 L (G1 X)
H5 : seq N1 L (G1 X)
============================
 seq (s N1) L (ex G1)

Subgoal 2.9 is:
 seq (s N1) L (atom A)

seq_lt < search.
Subgoal 2.9:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : prog A B
H5 : seq M1 L B
============================
 seq (s N1) L (atom A)

seq_lt < apply IH to H3 H5.
Subgoal 2.9:

Variables: L N1 M1 B A
IH : forall L G N M, lt M N * -> seq M L G -> seq N L G
H3 : lt M1 N1 *
H4 : prog A B
H5 : seq M1 L B
H6 : seq N1 L B
============================
 seq (s N1) L (atom A)

seq_lt < search.
Proof completed.
Abella < Theorem nat_lt : 
forall A B, nat A -> nat B -> lt A B \/ A = B \/ lt B A.


============================
 forall A B, nat A -> nat B -> lt A B \/ A = B \/ lt B A

nat_lt < induction on 1.

IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
============================
 forall A B, nat A @ -> nat B -> lt A B \/ A = B \/ lt B A

nat_lt < intros.

Variables: A B
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H1 : nat A @
H2 : nat B
============================
 lt A B \/ A = B \/ lt B A

nat_lt < case H1.
Subgoal 1:

Variables: B
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H2 : nat B
============================
 lt z B \/ z = B \/ lt B z

Subgoal 2 is:
 lt (s N) B \/ s N = B \/ lt B (s N)

nat_lt < case H2.
Subgoal 1.1:

IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
============================
 lt z z \/ z = z \/ lt z z

Subgoal 1.2 is:
 lt z (s N) \/ z = s N \/ lt (s N) z

Subgoal 2 is:
 lt (s N) B \/ s N = B \/ lt B (s N)

nat_lt < search.
Subgoal 1.2:

Variables: N
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N
============================
 lt z (s N) \/ z = s N \/ lt (s N) z

Subgoal 2 is:
 lt (s N) B \/ s N = B \/ lt B (s N)

nat_lt < search.
Subgoal 2:

Variables: B N
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H2 : nat B
H3 : nat N *
============================
 lt (s N) B \/ s N = B \/ lt B (s N)

nat_lt < case H2.
Subgoal 2.1:

Variables: N
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N *
============================
 lt (s N) z \/ s N = z \/ lt z (s N)

Subgoal 2.2 is:
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

nat_lt < search.
Subgoal 2.2:

Variables: N N1
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N *
H4 : nat N1
============================
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

nat_lt < apply IH to H3 H4.
Subgoal 2.2:

Variables: N N1
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N *
H4 : nat N1
H5 : lt N N1 \/ N = N1 \/ lt N1 N
============================
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

nat_lt < case H5.
Subgoal 2.2.1:

Variables: N N1
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N *
H4 : nat N1
H6 : lt N N1
============================
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

Subgoal 2.2.2 is:
 lt (s N1) (s N1) \/ s N1 = s N1 \/ lt (s N1) (s N1)

Subgoal 2.2.3 is:
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

nat_lt < search.
Subgoal 2.2.2:

Variables: N1
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N1 *
H4 : nat N1
============================
 lt (s N1) (s N1) \/ s N1 = s N1 \/ lt (s N1) (s N1)

Subgoal 2.2.3 is:
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

nat_lt < search.
Subgoal 2.2.3:

Variables: N N1
IH : forall A B, nat A * -> nat B -> lt A B \/ A = B \/ lt B A
H3 : nat N *
H4 : nat N1
H6 : lt N1 N
============================
 lt (s N) (s N1) \/ s N = s N1 \/ lt (s N1) (s N)

nat_lt < search.
Proof completed.
Abella < Theorem seq_cut : 
forall K L G N M, nat N -> seq N (cons K L) G -> nat M -> seq M L (atom K) ->
  (exists P, nat P /\ seq P L G).


============================
 forall K L G N M, nat N -> seq N (cons K L) G -> nat M ->
   seq M L (atom K) -> (exists P, nat P /\ seq P L G)

seq_cut < induction on 1.

IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
============================
 forall K L G N M, nat N @ -> seq N (cons K L) G -> nat M ->
   seq M L (atom K) -> (exists P, nat P /\ seq P L G)

seq_cut < intros.

Variables: K L G N M
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H1 : nat N @
H2 : seq N (cons K L) G
H3 : nat M
H4 : seq M L (atom K)
============================
 exists P, nat P /\ seq P L G

seq_cut < case H1.
Subgoal 1:

Variables: K L G M
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H2 : seq z (cons K L) G
H3 : nat M
H4 : seq M L (atom K)
============================
 exists P, nat P /\ seq P L G

Subgoal 2 is:
 exists P, nat P /\ seq P L G

seq_cut < case H2.
Subgoal 2:

Variables: K L G M N1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H2 : seq (s N1) (cons K L) G
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
============================
 exists P, nat P /\ seq P L G

seq_cut < case H2.
Subgoal 2.1:

Variables: K L M N1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
============================
 exists P, nat P /\ seq P L tt

Subgoal 2.2 is:
 exists P, nat P /\ seq P L (atom A)

Subgoal 2.3 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.4 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.2:

Variables: K L M N1 A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : mem A (cons K L)
============================
 exists P, nat P /\ seq P L (atom A)

Subgoal 2.3 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.4 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < case H6.
Subgoal 2.2.1:

Variables: K L M N1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
============================
 exists P, nat P /\ seq P L (atom K)

Subgoal 2.2.2 is:
 exists P, nat P /\ seq P L (atom A)

Subgoal 2.3 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.4 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.2.2:

Variables: K L M N1 A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H7 : mem A L
============================
 exists P, nat P /\ seq P L (atom A)

Subgoal 2.3 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.4 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.3:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
============================
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.4 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H6 H3 H4.
Subgoal 2.3:

Variables: K L M N1 B A P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : nat P
H8 : seq P L A
============================
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.4 is:
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.4:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) B
============================
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H6 H3 H4.
Subgoal 2.4:

Variables: K L M N1 B A P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) B
H7 : nat P
H8 : seq P L B
============================
 exists P, nat P /\ seq P L (or A B)

Subgoal 2.5 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.5:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H6 H3 H4.
Subgoal 2.5:

Variables: K L M N1 B A P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H7 H3 H4.
Subgoal 2.5:

Variables: K L M N1 B A P P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
H10 : nat P1
H11 : seq P1 L B
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply nat_lt to H8 H10.
Subgoal 2.5:

Variables: K L M N1 B A P P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
H10 : nat P1
H11 : seq P1 L B
H12 : lt P P1 \/ P = P1 \/ lt P1 P
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < case H12.
Subgoal 2.5.1:

Variables: K L M N1 B A P P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
H10 : nat P1
H11 : seq P1 L B
H13 : lt P P1
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.5.2 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.5.3 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply seq_lt to H13 H9.
Subgoal 2.5.1:

Variables: K L M N1 B A P P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
H10 : nat P1
H11 : seq P1 L B
H13 : lt P P1
H14 : seq P1 L A
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.5.2 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.5.3 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.5.2:

Variables: K L M N1 B A P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P1
H9 : seq P1 L A
H10 : nat P1
H11 : seq P1 L B
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.5.3 is:
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.5.3:

Variables: K L M N1 B A P P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
H10 : nat P1
H11 : seq P1 L B
H13 : lt P1 P
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply seq_lt to H13 H11.
Subgoal 2.5.3:

Variables: K L M N1 B A P P1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) A
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L A
H10 : nat P1
H11 : seq P1 L B
H13 : lt P1 P
H14 : seq P L B
============================
 exists P, nat P /\ seq P L (and A B)

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.6:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
============================
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < assert forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L)).
Subgoal 2.6.1:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
============================
 forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L))

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < intros.
Subgoal 2.6.1:

Variables: K L M N1 B A X
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H7 : mem X (cons A (cons K L))
============================
 mem X (cons K (cons A L))

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < case H7.
Subgoal 2.6.1.1:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
============================
 mem A (cons K (cons A L))

Subgoal 2.6.1.2 is:
 mem X (cons K (cons A L))

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.6.1.2:

Variables: K L M N1 B A X
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H8 : mem X (cons K L)
============================
 mem X (cons K (cons A L))

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < case H8.
Subgoal 2.6.1.2.1:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
============================
 mem K (cons K (cons A L))

Subgoal 2.6.1.2.2 is:
 mem X (cons K (cons A L))

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.6.1.2.2:

Variables: K L M N1 B A X
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H9 : mem X L
============================
 mem X (cons K (cons A L))

Subgoal 2.6 is:
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.6:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H7 : forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L))
============================
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply seq_subset to H6 H7.
Subgoal 2.6:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H7 : forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L))
H8 : seq N1 (cons K (cons A L)) B
============================
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < assert forall X, mem X L -> mem X (cons A L).
Subgoal 2.6:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H7 : forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L))
H8 : seq N1 (cons K (cons A L)) B
H9 : forall X, mem X L -> mem X (cons A L)
============================
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply seq_subset to H4 H9.
Subgoal 2.6:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H7 : forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L))
H8 : seq N1 (cons K (cons A L)) B
H9 : forall X, mem X L -> mem X (cons A L)
H10 : seq M (cons A L) (atom K)
============================
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H8 H3 H10.
Subgoal 2.6:

Variables: K L M N1 B A P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons A (cons K L)) B
H7 : forall X, mem X (cons A (cons K L)) -> mem X (cons K (cons A L))
H8 : seq N1 (cons K (cons A L)) B
H9 : forall X, mem X L -> mem X (cons A L)
H10 : seq M (cons A L) (atom K)
H11 : nat P
H12 : seq P (cons A L) B
============================
 exists P, nat P /\ seq P L (imp A B)

Subgoal 2.7 is:
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.7:

Variables: K L M N1 G1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) (G1 n1)
============================
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H6 H3 H4.
Subgoal 2.7:

Variables: K L M N1 G1 P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) (G1 n1)
H7 : nat P
H8 : seq P L (G1 n1)
============================
 exists P, nat P /\ seq P L (all G1)

Subgoal 2.8 is:
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.8:

Variables: K L M N1 X G1
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) (G1 X)
============================
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H6 H3 H4.
Subgoal 2.8:

Variables: K L M N1 X G1 P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : seq N1 (cons K L) (G1 X)
H7 : nat P
H8 : seq P L (G1 X)
============================
 exists P, nat P /\ seq P L (ex G1)

Subgoal 2.9 is:
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Subgoal 2.9:

Variables: K L M N1 B A
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : prog A B
H7 : seq N1 (cons K L) B
============================
 exists P, nat P /\ seq P L (atom A)

seq_cut < apply IH to H5 H7 H3 H4.
Subgoal 2.9:

Variables: K L M N1 B A P
IH : forall K L G N M, nat N * -> seq N (cons K L) G -> nat M ->
       seq M L (atom K) -> (exists P, nat P /\ seq P L G)
H3 : nat M
H4 : seq M L (atom K)
H5 : nat N1 *
H6 : prog A B
H7 : seq N1 (cons K L) B
H8 : nat P
H9 : seq P L B
============================
 exists P, nat P /\ seq P L (atom A)

seq_cut < search.
Proof completed.
Abella < Theorem mem_inst : 
forall L A T, nabla x, mem (A x) (L x) -> mem (A T) (L T).


============================
 forall L A T, nabla x, mem (A x) (L x) -> mem (A T) (L T)

mem_inst < induction on 1.

IH : forall L A T, nabla x, mem (A x) (L x) * -> mem (A T) (L T)
============================
 forall L A T, nabla x, mem (A x) (L x) @ -> mem (A T) (L T)

mem_inst < intros.

Variables: L A T
IH : forall L A T, nabla x, mem (A x) (L x) * -> mem (A T) (L T)
H1 : mem (A n1) (L n1) @
============================
 mem (A T) (L T)

mem_inst < case H1.
Subgoal 1:

Variables: A T L1
IH : forall L A T, nabla x, mem (A x) (L x) * -> mem (A T) (L T)
============================
 mem (A T) (cons (A T) (L1 T))

Subgoal 2 is:
 mem (A T) (cons (B T) (L1 T))

mem_inst < search.
Subgoal 2:

Variables: A T L1 B
IH : forall L A T, nabla x, mem (A x) (L x) * -> mem (A T) (L T)
H2 : mem (A n1) (L1 n1) *
============================
 mem (A T) (cons (B T) (L1 T))

mem_inst < apply IH to H2 with T = T.
Subgoal 2:

Variables: A T L1 B
IH : forall L A T, nabla x, mem (A x) (L x) * -> mem (A T) (L T)
H2 : mem (A n1) (L1 n1) *
H3 : mem (A T) (L1 T)
============================
 mem (A T) (cons (B T) (L1 T))

mem_inst < search.
Proof completed.
Abella < Theorem prog_inst : 
forall A B T, nabla x, prog (A x) (B x) -> prog (A T) (B T).


============================
 forall A B T, nabla x, prog (A x) (B x) -> prog (A T) (B T)

prog_inst < intros.

Variables: A B T
H1 : prog (A n1) (B n1)
============================
 prog (A T) (B T)

prog_inst < case H1.
Subgoal 1:

Variables: T R
============================
 prog (eval (abs (R T)) (abs (R T))) tt

Subgoal 2 is:
 prog (eval (app (P T) (Q T)) (V T))
   (and (atom (eval (P T) (abs (R T)))) (atom (eval (R T (Q T)) (V T))))

Subgoal 3 is:
 prog (of (abs (R T)) (arrow A1 B1))
   (all (x\imp (of x A1) (atom (of (R T x) B1))))

Subgoal 4 is:
 prog (of (app (P T) (Q T)) B1)
   (and (atom (of (P T) (arrow A1 B1))) (atom (of (Q T) A1)))

prog_inst < search.
Subgoal 2:

Variables: T V Q R P
============================
 prog (eval (app (P T) (Q T)) (V T))
   (and (atom (eval (P T) (abs (R T)))) (atom (eval (R T (Q T)) (V T))))

Subgoal 3 is:
 prog (of (abs (R T)) (arrow A1 B1))
   (all (x\imp (of x A1) (atom (of (R T x) B1))))

Subgoal 4 is:
 prog (of (app (P T) (Q T)) B1)
   (and (atom (of (P T) (arrow A1 B1))) (atom (of (Q T) A1)))

prog_inst < search.
Subgoal 3:

Variables: T B1 R A1
============================
 prog (of (abs (R T)) (arrow A1 B1))
   (all (x\imp (of x A1) (atom (of (R T x) B1))))

Subgoal 4 is:
 prog (of (app (P T) (Q T)) B1)
   (and (atom (of (P T) (arrow A1 B1))) (atom (of (Q T) A1)))

prog_inst < search.
Subgoal 4:

Variables: T A1 Q B1 P
============================
 prog (of (app (P T) (Q T)) B1)
   (and (atom (of (P T) (arrow A1 B1))) (atom (of (Q T) A1)))

prog_inst < search.
Proof completed.
Abella < Theorem seq_inst : 
forall N L G T, nabla x, seq N (L x) (G x) -> seq N (L T) (G T).


============================
 forall N L G T, nabla x, seq N (L x) (G x) -> seq N (L T) (G T)

seq_inst < induction on 1.

IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
============================
 forall N L G T, nabla x, seq N (L x) (G x) @ -> seq N (L T) (G T)

seq_inst < intros.

Variables: N L G T
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H1 : seq N (L n1) (G n1) @
============================
 seq N (L T) (G T)

seq_inst < case H1.
Subgoal 1:

Variables: L T N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
============================
 seq (s N1) (L T) tt

Subgoal 2 is:
 seq (s N1) (L T) (atom (A T))

Subgoal 3 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 4 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 2:

Variables: L T A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : mem (A n1) (L n1)
============================
 seq (s N1) (L T) (atom (A T))

Subgoal 3 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 4 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply mem_inst to H2 with T = T.
Subgoal 2:

Variables: L T A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : mem (A n1) (L n1)
H3 : mem (A T) (L T)
============================
 seq (s N1) (L T) (atom (A T))

Subgoal 3 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 4 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 3:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (A n1) *
============================
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 4 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H2 with T = T.
Subgoal 3:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (A n1) *
H3 : seq N1 (L T) (A T)
============================
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 4 is:
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 4:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (B n1) *
============================
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H2 with T = T.
Subgoal 4:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (B n1) *
H3 : seq N1 (L T) (B T)
============================
 seq (s N1) (L T) (or (A T) (B T))

Subgoal 5 is:
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 5:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (A n1) *
H3 : seq N1 (L n1) (B n1) *
============================
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H2 with T = T.
Subgoal 5:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (A n1) *
H3 : seq N1 (L n1) (B n1) *
H4 : seq N1 (L T) (A T)
============================
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H3 with T = T.
Subgoal 5:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (A n1) *
H3 : seq N1 (L n1) (B n1) *
H4 : seq N1 (L T) (A T)
H5 : seq N1 (L T) (B T)
============================
 seq (s N1) (L T) (and (A T) (B T))

Subgoal 6 is:
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 6:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (cons (A n1) (L n1)) (B n1) *
============================
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H2 with T = T.
Subgoal 6:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (cons (A n1) (L n1)) (B n1) *
H3 : seq N1 (cons (A T) (L T)) (B T)
============================
 seq (s N1) (L T) (imp (A T) (B T))

Subgoal 7 is:
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 7:

Variables: L T G1 N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (G1 n1 n2) *
============================
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H2 with T = T.
Subgoal 7:

Variables: L T G1 N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (G1 n1 n2) *
H3 : seq N1 (L T) (G1 T n2)
============================
 seq (s N1) (L T) (all (G1 T))

Subgoal 8 is:
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 8:

Variables: L T X G1 N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (G1 n1 (X n1)) *
============================
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H2 with T = T.
Subgoal 8:

Variables: L T X G1 N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : seq N1 (L n1) (G1 n1 (X n1)) *
H3 : seq N1 (L T) (G1 T (X T))
============================
 seq (s N1) (L T) (ex (G1 T))

Subgoal 9 is:
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Subgoal 9:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : prog (A n1) (B n1)
H3 : seq N1 (L n1) (B n1) *
============================
 seq (s N1) (L T) (atom (A T))

seq_inst < apply prog_inst to H2 with T = T.
Subgoal 9:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : prog (A n1) (B n1)
H3 : seq N1 (L n1) (B n1) *
H4 : prog (A T) (B T)
============================
 seq (s N1) (L T) (atom (A T))

seq_inst < apply IH to H3 with T = T.
Subgoal 9:

Variables: L T B A N1
IH : forall N L G T, nabla x, seq N (L x) (G x) * -> seq N (L T) (G T)
H2 : prog (A n1) (B n1)
H3 : seq N1 (L n1) (B n1) *
H4 : prog (A T) (B T)
H5 : seq N1 (L T) (B T)
============================
 seq (s N1) (L T) (atom (A T))

seq_inst < search.
Proof completed.
Abella < Theorem lt_s : 
forall A B, lt A B -> lt A (s B).


============================
 forall A B, lt A B -> lt A (s B)

lt_s < induction on 1.

IH : forall A B, lt A B * -> lt A (s B)
============================
 forall A B, lt A B @ -> lt A (s B)

lt_s < intros.

Variables: A B
IH : forall A B, lt A B * -> lt A (s B)
H1 : lt A B @
============================
 lt A (s B)

lt_s < case H1.
Subgoal 1:

Variables: N
IH : forall A B, lt A B * -> lt A (s B)
============================
 lt z (s (s N))

Subgoal 2 is:
 lt (s M) (s (s N))

lt_s < search.
Subgoal 2:

Variables: N M
IH : forall A B, lt A B * -> lt A (s B)
H2 : lt M N *
============================
 lt (s M) (s (s N))

lt_s < apply IH to H2.
Subgoal 2:

Variables: N M
IH : forall A B, lt A B * -> lt A (s B)
H2 : lt M N *
H3 : lt M (s N)
============================
 lt (s M) (s (s N))

lt_s < search.
Proof completed.
Abella < Theorem sr : 
forall E V A M N N', nat N' -> lt N N' -> seq N nl (atom (eval E V)) ->
  nat M -> seq M nl (atom (of E A)) ->
  (exists P, nat P /\ seq P nl (atom (of V A))).


============================
 forall E V A M N N', nat N' -> lt N N' -> seq N nl (atom (eval E V)) ->
   nat M -> seq M nl (atom (of E A)) ->
   (exists P, nat P /\ seq P nl (atom (of V A)))

sr < induction on 1.

IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
============================
 forall E V A M N N', nat N' @ -> lt N N' -> seq N nl (atom (eval E V)) ->
   nat M -> seq M nl (atom (of E A)) ->
   (exists P, nat P /\ seq P nl (atom (of V A)))

sr < intros.

Variables: E V A M N N'
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H1 : nat N' @
H2 : lt N N'
H3 : seq N nl (atom (eval E V))
H4 : nat M
H5 : seq M nl (atom (of E A))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H1.
Subgoal 1:

Variables: E V A M N
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt N z
H3 : seq N nl (atom (eval E V))
H4 : nat M
H5 : seq M nl (atom (of E A))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

Subgoal 2 is:
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H2.
Subgoal 2:

Variables: E V A M N N1
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt N (s N1)
H3 : seq N nl (atom (eval E V))
H4 : nat M
H5 : seq M nl (atom (of E A))
H6 : nat N1 *
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H3.
Subgoal 2.1:

Variables: E V A M N1 N2
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s N2) (s N1)
H4 : nat M
H5 : seq M nl (atom (of E A))
H6 : nat N1 *
H7 : mem (eval E V) nl
============================
 exists P, nat P /\ seq P nl (atom (of V A))

Subgoal 2.2 is:
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H7.
Subgoal 2.2:

Variables: E V A M N1 B N2
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s N2) (s N1)
H4 : nat M
H5 : seq M nl (atom (of E A))
H6 : nat N1 *
H7 : prog (eval E V) B
H8 : seq N2 nl B
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H7.
Subgoal 2.2.1:

Variables: A M N1 N2 R
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s N2) (s N1)
H4 : nat M
H5 : seq M nl (atom (of (abs R) A))
H6 : nat N1 *
H8 : seq N2 nl tt
============================
 exists P, nat P /\ seq P nl (atom (of (abs R) A))

Subgoal 2.2.2 is:
 exists P, nat P /\ seq P nl (atom (of V A))

sr < search.
Subgoal 2.2.2:

Variables: V A M N1 N2 Q R P
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s N2) (s N1)
H4 : nat M
H5 : seq M nl (atom (of (app P Q) A))
H6 : nat N1 *
H8 : seq N2 nl (and (atom (eval P (abs R))) (atom (eval (R Q) V)))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H8.
Subgoal 2.2.2:

Variables: V A M N1 Q R P N3
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s (s N3)) (s N1)
H4 : nat M
H5 : seq M nl (atom (of (app P Q) A))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H5.
Subgoal 2.2.2.1:

Variables: V A N1 Q R P N3 N4
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s (s N3)) (s N1)
H4 : nat (s N4)
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H11 : mem (of (app P Q) A) nl
============================
 exists P, nat P /\ seq P nl (atom (of V A))

Subgoal 2.2.2.2 is:
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H11.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 B1 N4
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s (s N3)) (s N1)
H4 : nat (s N4)
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H11 : prog (of (app P Q) A) B1
H12 : seq N4 nl B1
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H11.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 N4 A1
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s (s N3)) (s N1)
H4 : nat (s N4)
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H12 : seq N4 nl (and (atom (of P (arrow A1 A))) (atom (of Q A1)))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H12.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H2 : lt (s (s N3)) (s N1)
H4 : nat (s (s N5))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H2.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H4 : nat (s (s N5))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < apply lt_s to H15.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H4 : nat (s (s N5))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H16 : lt (s N3) (s N1)
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H16.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H4 : nat (s (s N5))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H4.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H18 : nat (s N5)
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H18.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < apply IH to H6 H17 H9 H19 H13.
Subgoal 2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 P1
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat P1
H21 : seq P1 nl (atom (of (abs R) (arrow A1 A)))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H21.
Subgoal 2.2.2.2.1:

Variables: V A N1 Q R P N3 A1 N5 N6
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat (s N6)
H22 : mem (of (abs R) (arrow A1 A)) nl
============================
 exists P, nat P /\ seq P nl (atom (of V A))

Subgoal 2.2.2.2.2 is:
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H22.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 B2 N6
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat (s N6)
H22 : prog (of (abs R) (arrow A1 A)) B2
H23 : seq N6 nl B2
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H22.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N6
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat (s N6)
H23 : seq N6 nl (all (x\imp (of x A1) (atom (of (R x) A))))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H23.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N7
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat (s (s N7))
H24 : seq N7 nl (imp (of n1 A1) (atom (of (R n1) A)))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H24.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat (s (s (s N8)))
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < apply seq_inst to H25 with T = Q.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H20 : nat (s (s (s N8)))
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
H26 : seq N8 (cons (of Q A1) nl) (atom (of (R Q) A))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H20.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
H26 : seq N8 (cons (of Q A1) nl) (atom (of (R Q) A))
H27 : nat (s (s N8))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H27.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
H26 : seq N8 (cons (of Q A1) nl) (atom (of (R Q) A))
H28 : nat (s N8)
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < case H28.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
H26 : seq N8 (cons (of Q A1) nl) (atom (of (R Q) A))
H29 : nat N8
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < apply seq_cut to H29 H26 H19 H14.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8 P2
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
H26 : seq N8 (cons (of Q A1) nl) (atom (of (R Q) A))
H29 : nat N8
H30 : nat P2
H31 : seq P2 nl (atom (of (R Q) A))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < apply IH to H6 H17 H10 H30 H31.
Subgoal 2.2.2.2.2:

Variables: V A N1 Q R P N3 A1 N5 N8 P2 P3
IH : forall E V A M N N', nat N' * -> lt N N' ->
       seq N nl (atom (eval E V)) -> nat M -> seq M nl (atom (of E A)) ->
       (exists P, nat P /\ seq P nl (atom (of V A)))
H6 : nat N1 *
H9 : seq N3 nl (atom (eval P (abs R)))
H10 : seq N3 nl (atom (eval (R Q) V))
H13 : seq N5 nl (atom (of P (arrow A1 A)))
H14 : seq N5 nl (atom (of Q A1))
H15 : lt (s N3) N1
H17 : lt N3 N1
H19 : nat N5
H25 : seq N8 (cons (of n1 A1) nl) (atom (of (R n1) A))
H26 : seq N8 (cons (of Q A1) nl) (atom (of (R Q) A))
H29 : nat N8
H30 : nat P2
H31 : seq P2 nl (atom (of (R Q) A))
H32 : nat P3
H33 : seq P3 nl (atom (of V A))
============================
 exists P, nat P /\ seq P nl (atom (of V A))

sr < search.
Proof completed.
Abella < Define tridot : atmlist -> o -> prop by 
tridot L G := exists N, nat N /\ seq N L G.

Abella < Theorem lem1 : 
forall L, tridot L tt.


============================
 forall L, tridot L tt

lem1 < intros.

Variables: L
============================
 tridot L tt

lem1 < search.
Proof completed.
Abella < Theorem lem2 : 
forall L G1 G2, tridot L G1 -> tridot L (or G1 G2).


============================
 forall L G1 G2, tridot L G1 -> tridot L (or G1 G2)

lem2 < intros.

Variables: L G1 G2
H1 : tridot L G1
============================
 tridot L (or G1 G2)

lem2 < case H1.

Variables: L G1 G2 N
H2 : nat N
H3 : seq N L G1
============================
 tridot L (or G1 G2)

lem2 < search.
Proof completed.
Abella < Theorem lem3 : 
forall L G1 G2, tridot L G2 -> tridot L (or G1 G2).


============================
 forall L G1 G2, tridot L G2 -> tridot L (or G1 G2)

lem3 < intros.

Variables: L G1 G2
H1 : tridot L G2
============================
 tridot L (or G1 G2)

lem3 < case H1.

Variables: L G1 G2 N
H2 : nat N
H3 : seq N L G2
============================
 tridot L (or G1 G2)

lem3 < search.
Proof completed.
Abella < Theorem lem4 : 
forall L G1 G2, tridot L G1 -> tridot L G2 -> tridot L (and G1 G2).


============================
 forall L G1 G2, tridot L G1 -> tridot L G2 -> tridot L (and G1 G2)

lem4 < intros.

Variables: L G1 G2
H1 : tridot L G1
H2 : tridot L G2
============================
 tridot L (and G1 G2)

lem4 < case H1.

Variables: L G1 G2 N
H2 : tridot L G2
H3 : nat N
H4 : seq N L G1
============================
 tridot L (and G1 G2)

lem4 < case H2.

Variables: L G1 G2 N N1
H3 : nat N
H4 : seq N L G1
H5 : nat N1
H6 : seq N1 L G2
============================
 tridot L (and G1 G2)

lem4 < apply nat_lt to H3 H5.

Variables: L G1 G2 N N1
H3 : nat N
H4 : seq N L G1
H5 : nat N1
H6 : seq N1 L G2
H7 : lt N N1 \/ N = N1 \/ lt N1 N
============================
 tridot L (and G1 G2)

lem4 < case H7.
Subgoal 1:

Variables: L G1 G2 N N1
H3 : nat N
H4 : seq N L G1
H5 : nat N1
H6 : seq N1 L G2
H8 : lt N N1
============================
 tridot L (and G1 G2)

Subgoal 2 is:
 tridot L (and G1 G2)

Subgoal 3 is:
 tridot L (and G1 G2)

lem4 < apply seq_lt to H8 H4.
Subgoal 1:

Variables: L G1 G2 N N1
H3 : nat N
H4 : seq N L G1
H5 : nat N1
H6 : seq N1 L G2
H8 : lt N N1
H9 : seq N1 L G1
============================
 tridot L (and G1 G2)

Subgoal 2 is:
 tridot L (and G1 G2)

Subgoal 3 is:
 tridot L (and G1 G2)

lem4 < search.
Subgoal 2:

Variables: L G1 G2 N1
H3 : nat N1
H4 : seq N1 L G1
H5 : nat N1
H6 : seq N1 L G2
============================
 tridot L (and G1 G2)

Subgoal 3 is:
 tridot L (and G1 G2)

lem4 < search.
Subgoal 3:

Variables: L G1 G2 N N1
H3 : nat N
H4 : seq N L G1
H5 : nat N1
H6 : seq N1 L G2
H8 : lt N1 N
============================
 tridot L (and G1 G2)

lem4 < apply seq_lt to H8 H6.
Subgoal 3:

Variables: L G1 G2 N N1
H3 : nat N
H4 : seq N L G1
H5 : nat N1
H6 : seq N1 L G2
H8 : lt N1 N
H9 : seq N L G2
============================
 tridot L (and G1 G2)

lem4 < search.
Proof completed.
Abella < Theorem lem5 : 
forall L A G, tridot (cons A L) G -> tridot L (imp A G).


============================
 forall L A G, tridot (cons A L) G -> tridot L (imp A G)

lem5 < intros.

Variables: L A G
H1 : tridot (cons A L) G
============================
 tridot L (imp A G)

lem5 < case H1.

Variables: L A G N
H2 : nat N
H3 : seq N (cons A L) G
============================
 tridot L (imp A G)

lem5 < search.
Proof completed.
Abella < Theorem lem6 : 
forall L G, (nabla x, tridot L (G x)) -> tridot L (all G).


============================
 forall L G, (nabla x, tridot L (G x)) -> tridot L (all G)

lem6 < intros.

Variables: L G
H1 : nabla x, tridot L (G x)
============================
 tridot L (all G)

lem6 < case H1.

Variables: L G
H2 : tridot L (G n1)
============================
 tridot L (all G)

lem6 < case H2.

Variables: L G N
H3 : nat N
H4 : seq N L (G n1)
============================
 tridot L (all G)

lem6 < search.
Proof completed.
Abella < Theorem lem7 : 
forall L G T, tridot L (G T) -> tridot L (ex G).


============================
 forall L G T, tridot L (G T) -> tridot L (ex G)

lem7 < intros.

Variables: L G T
H1 : tridot L (G T)
============================
 tridot L (ex G)

lem7 < case H1.

Variables: L G T N
H2 : nat N
H3 : seq N L (G T)
============================
 tridot L (ex G)

lem7 < search.
Proof completed.
Abella <