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

```
```Abella < Type z conat.

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

```
```Abella < CoDefine conat : conat -> prop by
conat z;
conat (s A) := conat A.

```
```Abella < CoDefine coeq : conat -> conat -> prop by
coeq z z;
coeq (s A) (s B) := coeq A B.

```
```Abella < CoDefine inf : conat -> prop by
inf (s A) := inf A.

```
```Abella < CoDefine coadd : conat -> conat -> conat -> prop by

```
```Abella < Theorem coeq_refl :
forall A, conat A -> coeq A A.

```
```
============================
forall A, conat A -> coeq A A

coeq_refl < coinduction.
```
```
CH : forall A, conat A -> coeq A A +
============================
forall A, conat A -> coeq A A #

coeq_refl < intros.
```
```
Variables: A
CH : forall A, conat A -> coeq A A +
H1 : conat A
============================
coeq A A #

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

CH : forall A, conat A -> coeq A A +
============================
coeq z z #

Subgoal 2 is:
coeq (s A1) (s A1) #

coeq_refl < search.
```
```Subgoal 2:

Variables: A1
CH : forall A, conat A -> coeq A A +
H2 : conat A1
============================
coeq (s A1) (s A1) #

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

Variables: A1
CH : forall A, conat A -> coeq A A +
H2 : conat A1
H3 : coeq A1 A1 +
============================
coeq (s A1) (s A1) #

coeq_refl < search.
Proof completed.
```
```Abella < Theorem coeq_sym :
forall A B, coeq A B -> coeq B A.

```
```
============================
forall A B, coeq A B -> coeq B A

coeq_sym < coinduction.
```
```
CH : forall A B, coeq A B -> coeq B A +
============================
forall A B, coeq A B -> coeq B A #

coeq_sym < intros.
```
```
Variables: A B
CH : forall A B, coeq A B -> coeq B A +
H1 : coeq A B
============================
coeq B A #

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

CH : forall A B, coeq A B -> coeq B A +
============================
coeq z z #

Subgoal 2 is:
coeq (s B1) (s A1) #

coeq_sym < search.
```
```Subgoal 2:

Variables: B1 A1
CH : forall A B, coeq A B -> coeq B A +
H2 : coeq A1 B1
============================
coeq (s B1) (s A1) #

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

Variables: B1 A1
CH : forall A B, coeq A B -> coeq B A +
H2 : coeq A1 B1
H3 : coeq B1 A1 +
============================
coeq (s B1) (s A1) #

coeq_sym < search.
Proof completed.
```
```Abella < Theorem coeq_trans :
forall A B C, coeq A B -> coeq B C -> coeq A C.

```
```
============================
forall A B C, coeq A B -> coeq B C -> coeq A C

coeq_trans < coinduction.
```
```
CH : forall A B C, coeq A B -> coeq B C -> coeq A C +
============================
forall A B C, coeq A B -> coeq B C -> coeq A C #

coeq_trans < intros.
```
```
Variables: A B C
CH : forall A B C, coeq A B -> coeq B C -> coeq A C +
H1 : coeq A B
H2 : coeq B C
============================
coeq A C #

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

Variables: C
CH : forall A B C, coeq A B -> coeq B C -> coeq A C +
H2 : coeq z C
============================
coeq z C #

Subgoal 2 is:
coeq (s A1) C #

coeq_trans < search.
```
```Subgoal 2:

Variables: C B1 A1
CH : forall A B C, coeq A B -> coeq B C -> coeq A C +
H2 : coeq (s B1) C
H3 : coeq A1 B1
============================
coeq (s A1) C #

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

Variables: B1 A1 B2
CH : forall A B C, coeq A B -> coeq B C -> coeq A C +
H3 : coeq A1 B1
H4 : coeq B1 B2
============================
coeq (s A1) (s B2) #

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

Variables: B1 A1 B2
CH : forall A B C, coeq A B -> coeq B C -> coeq A C +
H3 : coeq A1 B1
H4 : coeq B1 B2
H5 : coeq A1 B2 +
============================
coeq (s A1) (s B2) #

coeq_trans < search.
Proof completed.
```
```Abella < Theorem inf_plus_one :
forall A, inf A -> coeq A (s A).

```
```
============================
forall A, inf A -> coeq A (s A)

inf_plus_one < coinduction.
```
```
CH : forall A, inf A -> coeq A (s A) +
============================
forall A, inf A -> coeq A (s A) #

inf_plus_one < intros.
```
```
Variables: A
CH : forall A, inf A -> coeq A (s A) +
H1 : inf A
============================
coeq A (s A) #

inf_plus_one < case H1.
```
```
Variables: A1
CH : forall A, inf A -> coeq A (s A) +
H2 : inf A1
============================
coeq (s A1) (s (s A1)) #

inf_plus_one < apply CH to H2.
```
```
Variables: A1
CH : forall A, inf A -> coeq A (s A) +
H2 : inf A1
H3 : coeq A1 (s A1) +
============================
coeq (s A1) (s (s A1)) #

inf_plus_one < search.
Proof completed.
```
```Abella < Theorem coadd_det :
forall A B C D, coadd A B C -> coadd A B D -> coeq C D.

```
```
============================
forall A B C D, coadd A B C -> coadd A B D -> coeq C D

```
```
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
============================
forall A B C D, coadd A B C -> coadd A B D -> coeq C D #

```
```
Variables: A B C D
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H1 : coadd A B C
H2 : coadd A B D
============================
coeq C D #

```
```Subgoal 1:

Variables: B D C1 A1
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H2 : coadd (s A1) B D
H3 : coadd A1 B C1
============================
coeq (s C1) D #

Subgoal 2 is:
coeq (s C1) D #

Subgoal 3 is:
coeq z D #

```
```Subgoal 1:

Variables: B C1 A1 C2
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H3 : coadd A1 B C1
H4 : coadd A1 B C2
============================
coeq (s C1) (s C2) #

Subgoal 2 is:
coeq (s C1) D #

Subgoal 3 is:
coeq z D #

coadd_det < apply CH to H3 H4.
```
```Subgoal 1:

Variables: B C1 A1 C2
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H3 : coadd A1 B C1
H4 : coadd A1 B C2
H5 : coeq C1 C2 +
============================
coeq (s C1) (s C2) #

Subgoal 2 is:
coeq (s C1) D #

Subgoal 3 is:
coeq z D #

```
```Subgoal 2:

Variables: D C1 B1
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H2 : coadd z (s B1) D
H3 : coadd z B1 C1
============================
coeq (s C1) D #

Subgoal 3 is:
coeq z D #

```
```Subgoal 2:

Variables: C1 B1 C2
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H3 : coadd z B1 C1
H4 : coadd z B1 C2
============================
coeq (s C1) (s C2) #

Subgoal 3 is:
coeq z D #

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

Variables: C1 B1 C2
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H3 : coadd z B1 C1
H4 : coadd z B1 C2
H5 : coeq C1 C2 +
============================
coeq (s C1) (s C2) #

Subgoal 3 is:
coeq z D #

```
```Subgoal 3:

Variables: D
CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
H2 : coadd z z D
============================
coeq z D #

```
```Subgoal 3:

CH : forall A B C D, coadd A B C -> coadd A B D -> coeq C D +
============================
coeq z z #

Proof completed.
```
```Abella < Theorem coadd_z :
forall A, conat A -> coadd A z A.

```
```
============================
forall A, conat A -> coadd A z A

```
```
CH : forall A, conat A -> coadd A z A +
============================
forall A, conat A -> coadd A z A #

```
```
Variables: A
CH : forall A, conat A -> coadd A z A +
H1 : conat A
============================

```
```Subgoal 1:

CH : forall A, conat A -> coadd A z A +
============================

Subgoal 2 is:
coadd (s A1) z (s A1) #

```
```Subgoal 2:

Variables: A1
CH : forall A, conat A -> coadd A z A +
H2 : conat A1
============================
coadd (s A1) z (s A1) #

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

Variables: A1
CH : forall A, conat A -> coadd A z A +
H2 : conat A1
H3 : coadd A1 z A1 +
============================
coadd (s A1) z (s A1) #

Proof completed.
```
```Abella < Theorem coadd_inf1 :
forall A B C, inf A -> coadd A B C -> inf C.

```
```
============================
forall A B C, inf A -> coadd A B C -> inf C

```
```
CH : forall A B C, inf A -> coadd A B C -> inf C +
============================
forall A B C, inf A -> coadd A B C -> inf C #

```
```
Variables: A B C
CH : forall A B C, inf A -> coadd A B C -> inf C +
H1 : inf A
H2 : coadd A B C
============================
inf C #

```
```
Variables: B C A1
CH : forall A B C, inf A -> coadd A B C -> inf C +
H2 : coadd (s A1) B C
H3 : inf A1
============================
inf C #

```
```
Variables: B A1 C1
CH : forall A B C, inf A -> coadd A B C -> inf C +
H3 : inf A1
H4 : coadd A1 B C1
============================
inf (s C1) #

coadd_inf1 < apply CH to H3 H4.
```
```
Variables: B A1 C1
CH : forall A B C, inf A -> coadd A B C -> inf C +
H3 : inf A1
H4 : coadd A1 B C1
H5 : inf C1 +
============================
inf (s C1) #

Proof completed.
```
```Abella < Theorem coadd_inf2 :
forall A B C, conat A -> inf B -> coadd A B C -> inf C.

```
```
============================
forall A B C, conat A -> inf B -> coadd A B C -> inf C

```
```
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
============================
forall A B C, conat A -> inf B -> coadd A B C -> inf C #

```
```
Variables: A B C
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H1 : conat A
H2 : inf B
H3 : coadd A B C
============================
inf C #

```
```Subgoal 1:

Variables: B C1 A1
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H1 : conat (s A1)
H2 : inf B
H4 : coadd A1 B C1
============================
inf (s C1) #

Subgoal 2 is:
inf (s C1) #

Subgoal 3 is:
inf z #

```
```Subgoal 1:

Variables: B C1 A1
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H2 : inf B
H4 : coadd A1 B C1
H5 : conat A1
============================
inf (s C1) #

Subgoal 2 is:
inf (s C1) #

Subgoal 3 is:
inf z #

coadd_inf2 < apply CH to H5 H2 H4.
```
```Subgoal 1:

Variables: B C1 A1
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H2 : inf B
H4 : coadd A1 B C1
H5 : conat A1
H6 : inf C1 +
============================
inf (s C1) #

Subgoal 2 is:
inf (s C1) #

Subgoal 3 is:
inf z #

```
```Subgoal 2:

Variables: C1 B1
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H1 : conat z
H2 : inf (s B1)
H4 : coadd z B1 C1
============================
inf (s C1) #

Subgoal 3 is:
inf z #

```
```Subgoal 2:

Variables: C1 B1
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H1 : conat z
H4 : coadd z B1 C1
H5 : inf B1
============================
inf (s C1) #

Subgoal 3 is:
inf z #

coadd_inf2 < apply CH to H1 H5 H4.
```
```Subgoal 2:

Variables: C1 B1
CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H1 : conat z
H4 : coadd z B1 C1
H5 : inf B1
H6 : inf C1 +
============================
inf (s C1) #

Subgoal 3 is:
inf z #

```
```Subgoal 3:

CH : forall A B C, conat A -> inf B -> coadd A B C -> inf C +
H1 : conat z
H2 : inf z
============================
inf z #

```Abella <