diff --git a/lean/ECS/Components.lean b/lean/ECS/Components.lean
index 6b0b845..2e68fb0 100644
--- a/lean/ECS/Components.lean
+++ b/lean/ECS/Components.lean
@@ -217,3 +217,26 @@ instance : @ExplSet Unit Unit _ where
 
 instance : ExplDestroy Unit where
   explDestroy _ _ := return ()
+
+/-- A pseudostore used to produce components of type `Entity`.
+It always returns `true` for `explExists`, and echoes back the entity argument for `explGet`.
+It can be used in e.g. `cmap $ fun (a, ety : Entity) -> b` to access the current entity.
+--/
+inductive EntityStore where
+  | EntityStore
+
+axiom ElemEntityStore : ElemFam EntityStore = Entity
+instance : FamilyDef ElemFam EntityStore Entity := ⟨ElemEntityStore⟩
+
+axiom StorageEntity : StorageFam Entity = EntityStore
+instance : FamilyDef StorageFam Entity EntityStore := ⟨StorageEntity⟩
+
+instance : @Component Entity EntityStore Entity _ _ where
+  constraint := rfl
+
+instance : @Has w Entity EntityStore _ where
+  getStore := return .EntityStore
+
+instance : @ExplGet EntityStore Entity _ where
+  explGet _ ety := return ety
+  explExists _ _ := return true
diff --git a/lean/Examples/BouncingBall.lean b/lean/Examples/BouncingBall.lean
index 25f6748..3b85a1a 100644
--- a/lean/Examples/BouncingBall.lean
+++ b/lean/Examples/BouncingBall.lean
@@ -73,6 +73,12 @@ def deleteAt (pos : Vector2) (radius : Float) : Position → System World (Optio
     (← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
     then return none else return (some ⟨p⟩)
 
+/-- An alternative to `deleteAt` that explicitly deletes an entity --/
+def deleteAt' (pos : Vector2) (radius : Float) : Position × Entity → System World Unit
+  | (⟨p⟩, e) => do if
+    (← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
+    then destroy (Position × Velocity) e else return ()
+
 def update : System World Unit := do
   let c : Config ← get global
   if (← isMouseButtonPressed MouseButton.left) then