diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index ea3d2e418..82c28b3f0 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -315,11 +315,23 @@ where the returned result should go.
         ...
        </k>
 
-  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), SPAN))
-        => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND, SPAN)
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN))
+        => #execTerminatorCall({#projectedCallTy(I, PROJS, LOCALS)}:>Ty, lookupFunction({#projectedCallTy(I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
       <locals> LOCALS </locals>
+    requires isTy(#projectedCallTy(I, PROJS, LOCALS))
+    [preserves-definedness] // valid local indexing checked, projected call target must resolve to a Ty
+
+  syntax MaybeTy ::= #projectedCallTy(Int, ProjectionElems, List) [function, total]
+
+  rule #projectedCallTy(I, PROJS, LOCALS)
+    => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+
+  rule #projectedCallTy(_, _, _) => TyUnknown [owise]
 
   // Intrinsic function call - execute directly without state switching
   rule [termCallIntrinsic]:
diff --git a/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next.rs b/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next.rs
new file mode 100644
index 000000000..f50b540f3
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next.rs
@@ -0,0 +1,44 @@
+const MAX_SIGNERS: usize = 3;
+
+fn main() {
+    let _keep: fn() -> bool = repro;
+}
+
+fn account_key(signer: &AccountInfo<'_>) -> Pubkey {
+    *signer.key
+}
+
+#[inline(never)]
+#[no_mangle]
+pub fn repro() -> bool {
+    let k0 = Pubkey([1; 32]);
+    let k1 = Pubkey([2; 32]);
+    let k2 = Pubkey([3; 32]);
+    let n = 2usize;
+    let accounts = [
+        AccountInfo { key: &k0 },
+        AccountInfo { key: &k1 },
+        AccountInfo { key: &k2 },
+    ];
+    let multisig = Multisig {
+        signers: [k1, k2, k0],
+    };
+
+    accounts[1..]
+        .iter()
+        .map(account_key)
+        .eq(multisig.signers.iter().take(n).copied())
+}
+
+#[derive(Clone)]
+struct AccountInfo<'a> {
+    key: &'a Pubkey,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Pubkey([u8; 32]);
+
+#[derive(Clone, Debug)]
+struct Multisig {
+    signers: [Pubkey; MAX_SIGNERS],
+}
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 945002873..7e9b8cb0f 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -39,6 +39,7 @@
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
     'test_offset_from-fail': ['testing'],
     'iter-eq-copied-take-dereftruncate': ['repro'],
+    'spl-multisig-iter-eq-copied-next': ['repro'],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',