diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index d1c5bbd2..99cce575 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -195,6 +195,9 @@ class Discrete (α : Type _) [OFE α] where
   discrete_0 {x y : α} : x ≡{0}≡ y → x ≡ y
 export OFE.Discrete (discrete_0)
 
+instance [OFE α][Discrete α](x: α): DiscreteE x where
+  discrete := Discrete.discrete_0
+
 #rocq_ignore ofe_discrete_subrelation "Generalized-rewriting subrelation; not needed in Lean."
 
 /-- For discrete OFEs, `n`-equivalence implies equivalence for any `n`. -/
diff --git a/Iris/Iris/Instances/Lib/GhostMap.lean b/Iris/Iris/Instances/Lib/GhostMap.lean
new file mode 100644
index 00000000..66e3a545
--- /dev/null
+++ b/Iris/Iris/Instances/Lib/GhostMap.lean
@@ -0,0 +1,39 @@
+module
+
+public import Iris.Instances.IProp
+public import Iris.Std.HeapInstances
+
+namespace Iris
+
+open Iris Std HeapView
+
+class GhostMapG (GF : BundledGFunctors)(F K V: Type _)(H : Type _ → Type _)
+    [UFraction F][LawfulPartialMap H K] where
+  elem: ElemG GF (constOF (HeapView F K (Agree (LeibnizO V)) H))
+
+section definitions
+
+variable [UFraction F][LawfulPartialMap H K][hgm: GhostMapG GF F K V H]
+
+public def ghost_map_auth (γ : GName) (dq : DFrac F) (m : H V): IProp GF :=
+  iOwn (E := hgm.elem) γ
+    (HeapView.Auth dq (Iris.Std.PartialMap.map (fun x ↦ toAgree ⟨x⟩) m))
+
+public def ghost_map_elem (γ : GName) (dq : DFrac F) (k: K) (v: V): IProp GF :=
+  iOwn (E := hgm.elem) γ (HeapView.Frag k dq (toAgree ⟨v⟩))
+
+end definitions
+
+notation γ " ↪●MAP " dq m => ghost_map_auth γ dq m
+notation γ " ↪◯MAP[" k "]{" dq "}" v => ghost_map_elem γ dq k v
+
+section lemmas
+
+variable (F K V : Type _) (H : Type _ → Type _) [UFraction F] [LawfulPartialMap H K] [CMRA V]
+variable [hgm: GhostMapG GF F K V H]
+
+@[rocq_alias ghost_map_elem_timeless]
+instance (γ : GName)(k: K)(dq: DFrac F)(v: V): BI.Timeless (ghost_map_elem (hgm := hgm) γ dq k v) :=
+  iOwn_timeless (E := hgm.elem)
+
+end lemmas