Symmetrical simplification

[hferee]

Currently, contextual_simp_form simplifies conjunctions in an asymmetrical way. Plan:

• Fix The definition of contextual_simp_form:

| φ1 ∧ φ2 =>
    let ψ1 := choose_conj (contextual_simp_form Δ φ1) (contextual_simp_form (φ1 :: Δ) φ2) in
    let ψ2 := choose_conj (contextual_simp_form (φ2 :: Δ) φ1) (contextual_simp_form Δ φ2) in
    if decide (weight ψ1 ≤ weight ψ2) then ψ1 else ψ2

• Change the definition of choose_conj to be symmetrical too (and much simpler ; currently uses Provable_dec)
• prove choose_conj_topR (like choose_conj_topL)
• fix the rest of the proofs
• Check with benchmarks that this improves the simplifiying process overall

[hferee]

The chosen definition is not the one above, but choose_conj can still be simplified.

[hferee]

Currently, large conjunctions are quite long to simplify (~ 7 seconds for a conjunction of size 700).
See if replacing choose_conj with its naïve version improves this.