We want to prove
( L0
L1
L2
: List
)
append(append(L0 , L1) , L2) = append(L0 , append(L1 , L2)) .
We use
induction on
L0
to prove this goal.
For this, we use the
induction
scheme based on the signature
{
nil, cons
}
for
List.
Induction requires that we do the following:

Base case: prove the assertion for
L0
=
nil
.

Induction case: assume the assertion for
L0
=
L0
,
and then prove it for
L0
=
cons(N0 , L0)
.

Quantifier
elimination introduces the new constant(s)
l0
:
List
.

Implication
elimination
assumes

( L1
L2
: List
)
append(append(l0 , L1) , L2) = append(l0 , append(L1 , L2))
.


Quantifier
elimination introduces the new constant(s)
n0
:
Nat
.

Quantifier
elimination introduces the new constant(s)
l1, l2
:
List
.

We show
append(append(cons(n0 , l0) , l1) , l2) = append(cons(n0 , l0) , append(l1 , l2))
by reduction.
And thus the main goal is proved.
