bugfix: simplify_trivial_quantification used equalities under match branches
bugfix: simplify_trivial_quantification used equalities under match branches

The following could be proved correct:

type t = A | B
function f (x:'a) : 'a = x
predicate top = A = f A
lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end
lemma fail : false

ssaavedra/why3,ssaavedra/why3,ssaavedra/why3