Improve the extraction and the Lean backend

[sonmarcho]

This PR adds various improvements:

1. It improves the Lean backend, by modifying some tactics like extract_goal (which I use to extract the current goal as an auxiliary lemma) and tweaking some definitions of the Standard library.

2. It improves the quality of the extracted code in two ways:

• code which uses array index/update operations is now a lot cleaner (micro-pass simplify_array_slice_update)
• it adds a micro-pass simplify_duplicate_calls. The reason is that when writing code we often naturally write duplicate expressions. For instance, below we duplicate expression i + j:

let x = a[i + j];
let y = b[i + j];

In the generated code, this leads to:

let i1 <- i + j
let x <- a.index i1
let i2 <- i + j
let y <- b.index i2

In this code, we have to reason about the fact that i + j doesn't overflow twice. The simplify_duplicate_calls micro-pass deduplicates those expression in the pure model, leading to the following code:

let i1 <- i + j
let x <- a.index i1
let y <- b.index i1