LET_ELIM_TAC does not pull out stuff in a existential.

[ordinarymath]

Consider something like

  ?t. (let v = (FOO FOO2) in BAR t v)

Calling LET_ELIM_TAC causes you to get this.

   ∃t. ∀v. Abbrev (v = FOO FOO2) ⇒ BAR t v

Another case is this.

  ?t. (let (v1,v2) = (FOO FOO2) in BAR t v)

calling LET_ELIM_TAC gets you this

   ∃t. ∀v1 v2. FOO FOO2 = (v1,v2) ⇒ BAR t v

[mn200]

Needs the rewrite that says

(?t. !v. v = e ==> P v t) <=> (!v. v = e ==> ?t. P v t)

along with a “pair-y” version of the same.