Function qe_and_simplify 

pub fn qe_and_simplify<T: Types>(
    solver: &mut SuggestionSolver<T>,
    constraint: &FlatConstraint<T>,
    binder_consts: &[ConstDecl<T>],
) -> Result<Expr<T>, SuggestionSolverError>