diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 4b0470f02..29ca416c8 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -450,6 +450,26 @@ This is done without consideration of the validity of the Downcast[^downcast].
        </k>
 ```
 
+In context with pointer casts, the semantics handles the special case of a _transparent wrapper struct_:
+A pointer to a struct containing a single element can be cast to a pointer to the single element itself.
+While the pointer cast tries to insert and remove field projections to the singleton field,
+it is still possible that a field projection occurs on a value which is not an Aggregate (nor a union).
+This necessitates a special rule which allows the semantics to perform a field projection to field 0 as a Noop.
+The situation typically arises when the stored value is a pointer (`NonNull`), therefore the rule is restricted to this case.
+The context is populated with the correct field access data, so that write-backs will correct the stored value to an Aggregate.
+
+```k
+  rule <k> #traverseProjection(
+             DEST,
+             PtrLocal(_, _, _, _) #as VALUE,
+             projectionElemField(fieldIdx(0), TY) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, VALUE, PROJS, CtxField(variantIdx(0), ListItem(VALUE), 0, TY) CTXTS) ... </k>
+    [preserves-definedness, priority(100)]
+```
+
+
 #### Unions
 ```k
   // Case: Union is in same state as field projection
diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_1.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_1.rs
new file mode 100644
index 000000000..85190672d
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter_next_1.rs
@@ -0,0 +1,15 @@
+struct Thing { payload: u16 }
+
+fn main() {
+    let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload: 3}];
+
+    let mut i = a.iter();
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 1);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 2);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 3);
+    // let elem = i.next();
+    // assert!(elem.is_none());
+}
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs
new file mode 100644
index 000000000..70cf419f0
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs
@@ -0,0 +1,15 @@
+struct Thing { payload: u16 }
+
+fn main() {
+    let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload: 3}];
+
+    let mut i = a.iter();
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 1);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 2);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 3);
+    let elem = i.next();
+    assert!(elem.is_none());
+}
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
new file mode 100644
index 000000000..dcc3159dd
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (1990 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio
+    span: 146
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index a62488f8b..77f181b67 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -58,6 +58,7 @@
     'iterator-simple-fail',
     'unions-fail',
     'transmute-maybe-uninit-fail',
+    'iter_next_2-fail',
 ]