diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index ece4c9a3f..05df79d37 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -581,16 +581,22 @@ Therefore a heuristics is used here:
                // or the closure ref type pointee is missing from the type table
      andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
      andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))))
-     andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
+     andBool (
+               lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
+               orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty))
+             )
     [priority(45), preserves-definedness]
 
   syntax Bool ::= isTupleType ( TypeInfo ) [function, total]
                 | isRefType ( TypeInfo ) [function, total]
+                | isFunType ( TypeInfo ) [function, total]
   // -------------------------------------------------------
   rule isTupleType(typeInfoTupleType(_, _)) => true
   rule isTupleType(    _                  ) => false [owise]
   rule isRefType(typeInfoRefType(_)) => true
   rule isRefType(    _             ) => false [owise]
+  rule isFunType(typeInfoFunType(_)) => true
+  rule isFunType(    _             ) => false [owise]
 
   syntax KItem ::= #setTupleArgs ( Int , Value )
                  | #setTupleArgs ( Int , List )
diff --git a/kmir/src/tests/integration/data/prove-rs/closure-fnonce-single-arg.rs b/kmir/src/tests/integration/data/prove-rs/closure-fnonce-single-arg.rs
new file mode 100644
index 000000000..2f7bc948b
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/closure-fnonce-single-arg.rs
@@ -0,0 +1,12 @@
+fn apply<F: FnOnce(u8) -> u8>(f: F, v: u8) -> u8 {
+    f(v)
+}
+
+fn main() {
+    let _ = repro();
+}
+
+fn repro() -> u8 {
+    let f = |x: u8| x + 1;
+    apply(f, 41u8)
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/iter-copied-take-next-thunk-regression.rs b/kmir/src/tests/integration/data/prove-rs/iter-copied-take-next-thunk-regression.rs
new file mode 100644
index 000000000..5d9f0f5aa
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter-copied-take-next-thunk-regression.rs
@@ -0,0 +1,19 @@
+#[derive(Copy, Clone)]
+struct Pubkey([u8; 32]);
+
+fn main() {
+    let _keep: fn(usize) -> u8 = repro;
+}
+
+#[no_mangle]
+pub fn repro(n: usize) -> u8 {
+    let keys = [Pubkey([1; 32]); 11];
+    let mut it = keys.iter().take(n).copied();
+
+    if 1 <= n && n <= 11 {
+        let first = it.next().unwrap();
+        first.0[0]
+    } else {
+        0
+    }
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/iter-map-eq-copied-take-thunk-frontier-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter-map-eq-copied-take-thunk-frontier-fail.rs
new file mode 100644
index 000000000..14de11067
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter-map-eq-copied-take-thunk-frontier-fail.rs
@@ -0,0 +1,21 @@
+const TAKE_N: usize = 3;
+
+fn main() {
+    let _keep: fn(&[AccountInfo<'_>; 5], [Pubkey; 11]) -> bool = repro;
+}
+
+#[no_mangle]
+pub fn repro(accounts: &[AccountInfo<'_>; 5], signers: [Pubkey; 11]) -> bool {
+    accounts[2..]
+        .iter()
+        .map(|signer| *signer.key)
+        .eq(signers.iter().take(TAKE_N).copied())
+}
+
+#[derive(Clone)]
+struct AccountInfo<'a> {
+    key: &'a Pubkey,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Pubkey([u8; 32]);
diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-fnonce-single-arg.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-fnonce-single-arg.repro.expected
new file mode 100644
index 000000000..0df601d80
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/closure-fnonce-single-arg.repro.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (126 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter-copied-take-next-thunk-regression.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/iter-copied-take-next-thunk-regression.repro.expected
new file mode 100644
index 000000000..771f6807c
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/iter-copied-take-next-thunk-regression.repro.expected
@@ -0,0 +1,72 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (337 steps)
+├─ 3 (split)
+│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     notBool 1 <=Int ARG_UINT1:Int
+┃  │
+┃  ├─ 4
+┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+┃  │
+┃  │  (17 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     1 <=Int ARG_UINT1:Int
+   │
+   ├─ 5
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+   │
+   │  (27 steps)
+   ├─ 7 (split)
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+   ┃
+   ┃ (branch)
+   ┣━━┓ subst: .Subst
+   ┃  ┃ constraint:
+   ┃  ┃     notBool ARG_UINT1:Int <=Int 11
+   ┃  │
+   ┃  ├─ 8
+   ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+   ┃  │
+   ┃  │  (17 steps)
+   ┃  ├─ 10 (terminal)
+   ┃  │   #EndProgram ~> .K
+   ┃  │
+   ┃  ┊  constraint: true
+   ┃  ┊  subst: ...
+   ┃  └─ 2 (leaf, target, terminal)
+   ┃      #EndProgram ~> .K
+   ┃
+   ┗━━┓ subst: .Subst
+      ┃ constraint:
+      ┃     ARG_UINT1:Int <=Int 11
+      │
+      ├─ 9
+      │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+      │
+      │  (706 steps)
+      ├─ 11 (terminal)
+      │   #EndProgram ~> .K
+      │
+      ┊  constraint: true
+      ┊  subst: ...
+      └─ 2 (leaf, target, terminal)
+          #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter-map-eq-copied-take-thunk-frontier-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/iter-map-eq-copied-take-thunk-frontier-fail.repro.expected
new file mode 100644
index 000000000..72726db76
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/iter-map-eq-copied-take-thunk-frontier-fail.repro.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (867 steps)
+└─ 3 (stuck, leaf)
+    ListItem ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 88 ) , typeInf
+    span: 273
+
+
+┌─ 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 8b1def7f8..40b6b9bf6 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -38,6 +38,9 @@
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
     'test_offset_from-fail': ['testing'],
+    'closure-fnonce-single-arg': ['repro'],
+    'iter-copied-take-next-thunk-regression': ['repro'],
+    'iter-map-eq-copied-take-thunk-frontier-fail': ['repro'],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',
@@ -65,6 +68,7 @@
     'ref-ptr-cast-elem-offset-fail',
     'and_then_closure-fail',
     'closure_access_struct-fail',
+    'iter-map-eq-copied-take-thunk-frontier-fail',
 ]