diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index bcce7438b..f76620160 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1440,6 +1440,20 @@ which have the same representation `Value::Range`.
 Also, casts to and from _transparent wrappers_ (newtypes that just forward field `0`, i.e. `struct Wrapper<T>(T)`)
 are allowed, and supported by a special projection `WrapStruct`.
 
+When the source and target types are pointer types with the same pointee type (i.e., differing only in mutability),
+the cast preserves the source pointer and its metadata unchanged.
+
+```k
+  rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
+          => PtrLocal(OFFSET, PLACE, MUT, META)
+          ...
+        </k>
+      requires pointeeTy(lookupTy(TY_SOURCE)) ==K pointeeTy(lookupTy(TY_TARGET))
+      [priority(45), preserves-definedness] // valid map lookups checked
+```
+
+Otherwise, compute the type projection and convert metadata accordingly.
+
 ```k
   rule <k> #cast(PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
           =>
diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_3.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_3.rs
new file mode 100644
index 000000000..260b11cae
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter_next_3.rs
@@ -0,0 +1,19 @@
+struct Wrapper {
+    tag: u8,
+    a: [[u8; 32]; 3],
+}
+
+fn foo(c: &Wrapper) {
+    for elem in c.a.iter() {
+        assert!(elem[0] != 0);
+    }
+}
+
+fn main() {
+    let c = Wrapper {
+        tag: 42,
+        a: [[1u8; 32], [2u8; 32], [3u8; 32]],
+    };
+
+    foo(&c);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected
new file mode 100644
index 000000000..a4c5bdc3d
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (2028 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 5f36b155d..3014e4b04 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -43,6 +43,7 @@
     'local-raw-fail',
     'interior-mut-fail',
     'interior-mut3-fail',
+    'iter_next_3',
     'assert_eq_exp',
     'bitwise-not-shift',
     'symbolic-args-fail',