[sledge] Fix handling of existentials in Sh.and_
[sledge] Fix handling of existentials in Sh.and_

Summary:
`Sh.and_ b q` normalizes `b` using the equality context of `q` and
then conjoins the result to `q`. This is incorrect in case normalizing
`b` results in expressing it using existentials of `q`, which takes
the existentials out of their scope. So this diff changes from
essentially

    `(∃x.Q) ∧ B = (∃x.Q) ∧ (∃x.Bρ)`
to
    `(∃x.Q) ∧ B = (∃x'.Q[x'/x] ∧ Bρ)`

where `ρ` is the substitution that normalizes with respect to the
equality context.

Reviewed By: jvillard

Differential Revision: D26250536

fbshipit-source-id: 05f5c48c0

jvillard/infer,facebook/infer,facebook/infer,facebook/infer,jvillard/infer,facebook/infer,facebook/infer,jvillard/infer,jvillard/infer,facebook/infer,facebook/infer,jvillard/infer,jvillard/infer,jvillard/infer