Make `iPureIntro` able to introduce affine pure assertions when the context is emtpy.
The current lemma behind iPureIntro is:
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.