Consider Insertion into Doubly-Linked List.

Simplify the program.

Compute verification conditions.

Simplify (parts of) verification conditions.

Give them to the prover.