simplify_trivial_quantifier va moins sous les triggers (il peut encore remplacer dessous mais pas y trouver d'égalité)