Welcome to Abella 2.0.5-dev.
```Abella < Kind nat type.

```
```Abella < Type z nat.

```
```Abella < Type s nat -> nat.

```
```Abella < CoDefine colist : olist -> prop by
colist nil;
colist (X :: L) := colist L.

```
```Abella < CoDefine eqi : olist -> olist -> prop by
eqi nil nil;
eqi (X :: L) (X :: R) := eqi L R.

```
```Abella < Define tk : nat -> olist -> olist -> prop by
tk z L nil;
tk N nil nil;
tk (s N) (X :: L) (X :: R) := tk N L R.

```
```Abella < Define eqf : olist -> olist -> prop by
eqf L R := (forall N S, tk N L S -> tk N R S) /\ (forall N S, tk N R S -> tk N L S).

```
```Abella < Theorem eqi_take :
forall L R S N, eqi L R -> tk N L S -> tk N R S.

```
```
============================
forall L R S N, eqi L R -> tk N L S -> tk N R S

eqi_take < induction on 2.
```
```
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
============================
forall L R S N, eqi L R -> tk N L S @ -> tk N R S

eqi_take < intros.
```
```
Variables: L R S N
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi L R
H2 : tk N L S @
============================
tk N R S

eqi_take < case H2.
```
```Subgoal 1:

Variables: L R
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi L R
============================
tk z R nil

Subgoal 2 is:
tk N R nil

Subgoal 3 is:
tk (s N1) R (X :: R1)

eqi_take < search.
```
```Subgoal 2:

Variables: R N
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi nil R
============================
tk N R nil

Subgoal 3 is:
tk (s N1) R (X :: R1)

eqi_take < case H1.
```
```Subgoal 2:

Variables: N
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
============================
tk N nil nil

Subgoal 3 is:
tk (s N1) R (X :: R1)

eqi_take < search.
```
```Subgoal 3:

Variables: R R1 X L1 N1
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi (X :: L1) R
H3 : tk N1 L1 R1 *
============================
tk (s N1) R (X :: R1)

eqi_take < case H1.
```
```Subgoal 3:

Variables: R1 X L1 N1 R2
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H3 : tk N1 L1 R1 *
H4 : eqi L1 R2
============================
tk (s N1) (X :: R2) (X :: R1)

eqi_take < apply IH to H4 H3.
```
```Subgoal 3:

Variables: R1 X L1 N1 R2
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H3 : tk N1 L1 R1 *
H4 : eqi L1 R2
H5 : tk N1 R2 R1
============================
tk (s N1) (X :: R2) (X :: R1)

eqi_take < search.
Proof completed.
```
```Abella < Theorem eqi_sym :
forall L R, eqi L R -> eqi R L.

```
```
============================
forall L R, eqi L R -> eqi R L

eqi_sym < coinduction.
```
```
CH : forall L R, eqi L R -> eqi R L +
============================
forall L R, eqi L R -> eqi R L #

eqi_sym < intros.
```
```
Variables: L R
CH : forall L R, eqi L R -> eqi R L +
H1 : eqi L R
============================
eqi R L #

eqi_sym < case H1.
```
```Subgoal 1:

CH : forall L R, eqi L R -> eqi R L +
============================
eqi nil nil #

Subgoal 2 is:
eqi (X :: R1) (X :: L1) #

eqi_sym < search.
```
```Subgoal 2:

Variables: R1 X L1
CH : forall L R, eqi L R -> eqi R L +
H2 : eqi L1 R1
============================
eqi (X :: R1) (X :: L1) #

eqi_sym < apply CH to H2.
```
```Subgoal 2:

Variables: R1 X L1
CH : forall L R, eqi L R -> eqi R L +
H2 : eqi L1 R1
H3 : eqi R1 L1 +
============================
eqi (X :: R1) (X :: L1) #

eqi_sym < search.
Proof completed.
```
```Abella < Theorem eqi_eqf :
forall L R, eqi L R -> eqf L R.

```
```
============================
forall L R, eqi L R -> eqf L R

eqi_eqf < intros.
```
```
Variables: L R
H1 : eqi L R
============================
eqf L R

eqi_eqf < unfold.
```
```Subgoal 1:

Variables: L R
H1 : eqi L R
============================
forall N S, tk N L S -> tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqi_eqf < intros.
```
```Subgoal 1:

Variables: L R N S
H1 : eqi L R
H2 : tk N L S
============================
tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqi_eqf < apply eqi_take to H1 H2.
```
```Subgoal 1:

Variables: L R N S
H1 : eqi L R
H2 : tk N L S
H3 : tk N R S
============================
tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqi_eqf < search.
```
```Subgoal 2:

Variables: L R
H1 : eqi L R
============================
forall N S, tk N R S -> tk N L S

eqi_eqf < intros.
```
```Subgoal 2:

Variables: L R N S
H1 : eqi L R
H2 : tk N R S
============================
tk N L S

eqi_eqf < apply eqi_sym to H1.
```
```Subgoal 2:

Variables: L R N S
H1 : eqi L R
H2 : tk N R S
H3 : eqi R L
============================
tk N L S

eqi_eqf < apply eqi_take to H3 H2.
```
```Subgoal 2:

Variables: L R N S
H1 : eqi L R
H2 : tk N R S
H3 : eqi R L
H4 : tk N L S
============================
tk N L S

eqi_eqf < search.
Proof completed.
```
```Abella < Theorem eqf_nil :
forall L, eqf nil L -> L = nil.

```
```
============================
forall L, eqf nil L -> L = nil

eqf_nil < intros.
```
```
Variables: L
H1 : eqf nil L
============================
L = nil

eqf_nil < case H1.
```
```
Variables: L
H2 : forall N S, tk N nil S -> tk N L S
H3 : forall N S, tk N L S -> tk N nil S
============================
L = nil

eqf_nil < apply H2 to _ with N = s z.
```
```
Variables: L
H2 : forall N S, tk N nil S -> tk N L S
H3 : forall N S, tk N L S -> tk N nil S
H4 : tk (s z) L nil
============================
L = nil

eqf_nil < case H4.
```
```
H2 : forall N S, tk N nil S -> tk N nil S
H3 : forall N S, tk N nil S -> tk N nil S
============================
nil = nil

eqf_nil < search.
Proof completed.
```
```Abella < Theorem eqf_cons :
forall X L R, eqf (X :: L) R -> (exists S, R = X :: S).

```
```
============================
forall X L R, eqf (X :: L) R -> (exists S, R = X :: S)

eqf_cons < intros.
```
```
Variables: X L R
H1 : eqf (X :: L) R
============================
exists S, R = X :: S

eqf_cons < case H1.
```
```
Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N R S
H3 : forall N S, tk N R S -> tk N (X :: L) S
============================
exists S, R = X :: S

eqf_cons < apply H2 to _ with N = s z.
```
```
Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N R S
H3 : forall N S, tk N R S -> tk N (X :: L) S
H4 : tk (s z) R (X :: nil)
============================
exists S, R = X :: S

eqf_cons < case H4.
```
```
Variables: X L L1
H2 : forall N S, tk N (X :: L) S -> tk N (X :: L1) S
H3 : forall N S, tk N (X :: L1) S -> tk N (X :: L) S
H5 : tk z L1 nil
============================
exists S, X :: L1 = X :: S

eqf_cons < search.
Proof completed.
```
```Abella < Theorem eqf_sym :
forall L R, eqf L R -> eqf R L.

```
```
============================
forall L R, eqf L R -> eqf R L

eqf_sym < intros.
```
```
Variables: L R
H1 : eqf L R
============================
eqf R L

eqf_sym < case H1.
```
```
Variables: L R
H2 : forall N S, tk N L S -> tk N R S
H3 : forall N S, tk N R S -> tk N L S
============================
eqf R L

eqf_sym < search.
Proof completed.
```
```Abella < Theorem eqf_downward :
forall X L R, eqf (X :: L) (X :: R) -> eqf L R.

```
```
============================
forall X L R, eqf (X :: L) (X :: R) -> eqf L R

eqf_downward < intros.
```
```
Variables: X L R
H1 : eqf (X :: L) (X :: R)
============================
eqf L R

eqf_downward < case H1.
```
```
Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
============================
eqf L R

eqf_downward < unfold.
```
```Subgoal 1:

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
============================
forall N S, tk N L S -> tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqf_downward < intros.
```
```Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
============================
tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqf_downward < assert tk (s N) (X :: L) (X :: S).
```
```Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
H5 : tk (s N) (X :: L) (X :: S)
============================
tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqf_downward < apply H2 to H5.
```
```Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
H5 : tk (s N) (X :: L) (X :: S)
H6 : tk (s N) (X :: R) (X :: S)
============================
tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqf_downward < case H6.
```
```Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
H5 : tk (s N) (X :: L) (X :: S)
H7 : tk N R S
============================
tk N R S

Subgoal 2 is:
forall N S, tk N R S -> tk N L S

eqf_downward < search.
```
```Subgoal 2:

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
============================
forall N S, tk N R S -> tk N L S

eqf_downward < intros.
```
```Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
============================
tk N L S

eqf_downward < assert tk (s N) (X :: R) (X :: S).
```
```Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
H5 : tk (s N) (X :: R) (X :: S)
============================
tk N L S

eqf_downward < apply H3 to H5.
```
```Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
H5 : tk (s N) (X :: R) (X :: S)
H6 : tk (s N) (X :: L) (X :: S)
============================
tk N L S

eqf_downward < case H6.
```
```Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
H5 : tk (s N) (X :: R) (X :: S)
H7 : tk N L S
============================
tk N L S

eqf_downward < search.
Proof completed.
```
```Abella < Theorem eqf_eqi :
forall L R, colist L -> eqf L R -> eqi L R.

```
```
============================
forall L R, colist L -> eqf L R -> eqi L R

eqf_eqi < coinduction.
```
```
CH : forall L R, colist L -> eqf L R -> eqi L R +
============================
forall L R, colist L -> eqf L R -> eqi L R #

eqf_eqi < intros.
```
```
Variables: L R
CH : forall L R, colist L -> eqf L R -> eqi L R +
H1 : colist L
H2 : eqf L R
============================
eqi L R #

eqf_eqi < case H1.
```
```Subgoal 1:

Variables: R
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf nil R
============================
eqi nil R #

Subgoal 2 is:
eqi (X :: L1) R #

eqf_eqi < apply eqf_nil to H2.
```
```Subgoal 1:

CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf nil nil
============================
eqi nil nil #

Subgoal 2 is:
eqi (X :: L1) R #

eqf_eqi < search.
```
```Subgoal 2:

Variables: R L1 X
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) R
H3 : colist L1
============================
eqi (X :: L1) R #

eqf_eqi < apply eqf_cons to H2.
```
```Subgoal 2:

Variables: L1 X S
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) (X :: S)
H3 : colist L1
============================
eqi (X :: L1) (X :: S) #

eqf_eqi < apply eqf_downward to H2.
```
```Subgoal 2:

Variables: L1 X S
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) (X :: S)
H3 : colist L1
H4 : eqf L1 S
============================
eqi (X :: L1) (X :: S) #

eqf_eqi < apply CH to H3 H4.
```
```Subgoal 2:

Variables: L1 X S
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) (X :: S)
H3 : colist L1
H4 : eqf L1 S
H5 : eqi L1 S +
============================
eqi (X :: L1) (X :: S) #

eqf_eqi < search.
Proof completed.
```
```Abella < CoDefine coapp : olist -> olist -> olist -> prop by
coapp (X :: A) B (X :: C) := coapp A B C;
coapp nil (X :: B) (X :: C) := coapp nil B C;
coapp nil nil nil.

```
```Abella < Theorem coapp_assoc :
forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC -> coapp B C BC ->
coapp A BC ABC.

```
```
============================
forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC -> coapp B C BC ->
coapp A BC ABC

coapp_assoc < coinduction.
```
```
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
============================
forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC -> coapp B C BC ->
coapp A BC ABC #

coapp_assoc < intros.
```
```
Variables: A B C AB ABC BC
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H1 : coapp A B AB
H2 : coapp AB C ABC
H3 : coapp B C BC
============================
coapp A BC ABC #

coapp_assoc < case H1.
```
```Subgoal 1:

Variables: B C ABC BC C1 X A1
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H2 : coapp (X :: C1) C ABC
H3 : coapp B C BC
H4 : coapp A1 B C1
============================
coapp (X :: A1) BC ABC #

Subgoal 2 is:
coapp nil BC ABC #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < case H2.
```
```Subgoal 1:

Variables: B C BC C1 X A1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H3 : coapp B C BC
H4 : coapp A1 B C1
H5 : coapp C1 C C2
============================
coapp (X :: A1) BC (X :: C2) #

Subgoal 2 is:
coapp nil BC ABC #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < apply CH to H4 H5 H3.
```
```Subgoal 1:

Variables: B C BC C1 X A1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H3 : coapp B C BC
H4 : coapp A1 B C1
H5 : coapp C1 C C2
H6 : coapp A1 BC C2 +
============================
coapp (X :: A1) BC (X :: C2) #

Subgoal 2 is:
coapp nil BC ABC #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < search.
```
```Subgoal 2:

Variables: C ABC BC C1 X B1
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H2 : coapp (X :: C1) C ABC
H3 : coapp (X :: B1) C BC
H4 : coapp nil B1 C1
============================
coapp nil BC ABC #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < case H2.
```
```Subgoal 2:

Variables: C BC C1 X B1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H3 : coapp (X :: B1) C BC
H4 : coapp nil B1 C1
H5 : coapp C1 C C2
============================
coapp nil BC (X :: C2) #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < case H3.
```
```Subgoal 2:

Variables: C C1 X B1 C2 C3
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp C1 C C2
H6 : coapp B1 C C3
============================
coapp nil (X :: C3) (X :: C2) #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < apply CH to H4 H5 H6.
```
```Subgoal 2:

Variables: C C1 X B1 C2 C3
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp C1 C C2
H6 : coapp B1 C C3
H7 : coapp nil C3 C2 +
============================
coapp nil (X :: C3) (X :: C2) #

Subgoal 3 is:
coapp nil BC ABC #

coapp_assoc < search.
```
```Subgoal 3:

Variables: C ABC BC
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H2 : coapp nil C ABC
H3 : coapp nil C BC
============================
coapp nil BC ABC #

coapp_assoc < case H2.
```
```Subgoal 3.1:

Variables: BC C1 X B1
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H3 : coapp nil (X :: B1) BC
H4 : coapp nil B1 C1
============================
coapp nil BC (X :: C1) #

Subgoal 3.2 is:
coapp nil BC nil #

coapp_assoc < case H3.
```
```Subgoal 3.1:

Variables: C1 X B1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp nil B1 C2
============================
coapp nil (X :: C2) (X :: C1) #

Subgoal 3.2 is:
coapp nil BC nil #

coapp_assoc < apply CH to _ H4 H5.
```
```Subgoal 3.1:

Variables: C1 X B1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp nil B1 C2
H6 : coapp nil C2 C1 +
============================
coapp nil (X :: C2) (X :: C1) #

Subgoal 3.2 is:
coapp nil BC nil #

coapp_assoc < search.
```
```Subgoal 3.2:

Variables: BC
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
H3 : coapp nil nil BC
============================
coapp nil BC nil #

coapp_assoc < case H3.
```
```Subgoal 3.2:

CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
coapp B C BC -> coapp A BC ABC +
============================
coapp nil nil nil #

coapp_assoc < search.
Proof completed.
```
```Abella <
```