We want to prove
( L1
L2
L3
: List
)
append(append(L1 , L2) , L3) = append(L1 , append(L2 , L3)) .
We use induction on
L1
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
L1
=
nil
.

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

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

Implication elimination
assumes
( L2
L3
: List
)
append(append(l0 , L2) , L3) = append(l0 , append(L2 , L3))
.

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

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

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