Draft: Replace axiomatic lists with standard Why3 lists in WP plugin

This is a follow-up to the discussion from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.

Replaced an axiomatic definition of lists with the standard Why3 one:

• used standard Why3 list modules;
• replaced a declared list type with the standard one;
• provided definitions of all previously specified list functions except for repeat_box;
• replaced all axioms with lemmas except for those related to repeat_box;
• proved all new lemmas with Alt-Ergo and Isabelle/HOL;
• added Why3 session with Why3 realization files and associated Isabelle/HOL theories.

Facts nth_cons and nth_concat received a new premise for the index 0 <= k. All other facts have been kept intact.