Add lemmas and definitions from Alethe development

[NotBad4U]

Hi everyone,

This PR add some theorems and lemmas used for the Alethe development.

Bool.lp: imp, xorb, if-then-else lemmas
Epsilon.lp: εₑ
HOL.lp: transport
List.lp: foldl/foldr, mergesort and its correctness
Nat.lp: parity, div2, bitwise ops, strong induction
Pos.lp: multiplication lemmas
Prod.lp: sum type, dependent pairs, product lemmas
Z.lp: multiplication, power, comparison lemmas

This PR does not include Rational, Reals and bitvector because they depend on #72

🌊.....

[NotBad4U]

Maybe @melanie-taprogge, you can help @fblanqui review this one since this PR adds 2k lines.

[fblanqui]

Thank you very much Alessio for this PR! Here are my comments. Please merge master in your PR and update CHANGES.md too.

[NotBad4U]

Ok normally I resolved all your comments that I all agree.
I refined the require in files to avoid the maximum of dependencies.

Just one last point about builtins

builtin "0" ≔ _0;
builtin "1" ≔ _1;
builtin "2" ≔ _2;
builtin "3" ≔ _3;
builtin "4" ≔ _4;
builtin "5" ≔ _5;
builtin "6" ≔ _6;
builtin "7" ≔ _7;
builtin "8" ≔ _8;
builtin "9" ≔ _9;
builtin "10" ≔ _10;

Do you want to put them just after builtin "*" ≔ * or at the end of the file?

Or even I put back the builtin +, * and the one for digits at the end of the file ?

[fblanqui]

CI fails ...

[NotBad4U]

My bad, I think the lsp tricked me and I forgot to run make.