Make `iPureIntro` able to introduce affine pure assertions when the context is emtpy.
The current lemma behind
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q. Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
Could we change it a bit, so that we ask for
FromPure true Q φ when the context is empty? That way, we could introduce CFML's affine pure assertions transparently when the context is empty.