Make iFrame also instantiate telescopic existential quantifiers
Follow up on !1017 (merged): it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications ∃.. x
.
The initial attempt worked partly:
Global Instance frame_texist {TT : tele@{bi.Quant}} p R (Φ : TT → PROP)
(C : tele@{bi.Quant}) (g : C → TT) (Ψ : C → PROP) Q :
(∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
TCCbnSimplTele (∃.. c, Ψ c)%I Q →
Frame p R (∃.. x, Φ x) Q.
Proof.
move=> H HQ. rewrite /FrameTExists /Frame (bi_texist_exist Φ).
by eapply frame_exist.
Qed.
but this turns a telescopic quantifier into a regular one whenever things get framed beneath it.
We did not yet figure out a nice way to fix this.