iInstr on load with persistent points-to

[Armael]

Currently it requires manually moving the persistent points-to from the persistent context to the spatial context, then back after iInstr.
Solving the issue requires:

• the following patch to proofmode.v

@@ -317,13 +322,29 @@ Qed.
 Class EnvsLookupSpatial {PROP: bi} (Δ: envs PROP) (P: PROP) (i: ident) := {}.
 #[export] Hint Mode EnvsLookupSpatial + ! ! - : typeclass_instances.

-Instance EnvsLookupSpatial_here (PROP: bi) (Γp Γs: env PROP) P c i :
-  EnvsLookupSpatial (Envs Γp (Esnoc Γs i P) c) P i.
+Class EnvsLookupIntuitionistic {PROP: bi} (Δ: envs PROP) (P: PROP) (i: ident) := {}.
+#[export] Hint Mode EnvsLookupIntuitionistic + ! ! - : typeclass_instances.
+
+Class EnvLookup {PROP: bi} (Γ: env PROP) (P: PROP) (i: ident) := {}.
+#[export] Hint Mode EnvLookup + ! ! - : typeclass_instances.
+
+Instance EnvsLookupSpatial_default (PROP: bi) (Γp Γs: env PROP) P c i :
+  EnvLookup Γs P i →
+  EnvsLookupSpatial (Envs Γp Γs c) P i.
+Qed.
+
+Instance EnvsLookupIntuitionistic_default (PROP: bi) (Γp Γs: env PROP) P c i :
+  EnvLookup Γp P i →
+  EnvsLookupIntuitionistic (Envs Γp Γs c) P i.
+Qed.
+
+Instance EnvLookup_here (PROP: bi) (Γ: env PROP) P i :
+  EnvLookup (Esnoc Γ i P) P i.
 Qed.

-Instance EnvsLookupSpatial_next (PROP: bi) (Γp Γs: env PROP) P Q c i j :
-  EnvsLookupSpatial (Envs Γp Γs c) Q j →
-  EnvsLookupSpatial (Envs Γp (Esnoc Γs i P) c) Q j.
+Instance EnvLookup_next (PROP: bi) (Γ: env PROP) P Q i j :
+  EnvLookup Γ Q j →
+  EnvLookup (Esnoc Γ i P) Q j.
 Qed.

 Class FramableMachineResource {Σ: gFunctors} (P: iProp Σ) := {}.
@@ -358,7 +379,7 @@ Class FramableMachineHyp {Σ} (Δ: envs (uPredI (iResUR Σ))) (G: iProp Σ) (i:
 #[export] Hint Mode FramableMachineHyp + ! ! - : typeclass_instances.
 Instance FramableMachineHyp_default Σ (Δ: envs (uPredI (iResUR Σ))) G P i:
   LookupFramableMachineResource G P →
-  EnvsLookupSpatial Δ P i →
+  TCOr (EnvsLookupSpatial Δ P i) (EnvsLookupIntuitionistic Δ P i) →
   FramableMachineHyp Δ G i.
 Qed.

• understanding how to deal with the fact that iNamed currently fails when trying to intro a (persistent) fact "H" when there is already one in the persistent context. -> Contact Tej?.