diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index 05df79d37..5a2b48c65 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -548,8 +548,10 @@ Therefore a heuristics is used here:
      andBool isTypedValue(LOCALS[TUPLE])
      andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
      andBool isTypedLocal(LOCALS[CLOSURE])
-     andBool typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
-              // either the closure ref type is missing from type table
+     andBool (
+               typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
+               orBool isFunType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
+             )
     [priority(40), preserves-definedness]
 
   rule [setupCalleeClosure2]: <k> #setUpCalleeData(
diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected
index 60dbf8403..544958705 100644
--- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected
+++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (740 steps)
+│  (737 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │
diff --git a/kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs b/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/and_then_closure.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs b/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs
new file mode 100644
index 000000000..18cfb9c22
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs
@@ -0,0 +1,8 @@
+fn apply<F: FnOnce(u8, u8) -> u8>(f: F, a: u8, b: u8) -> u8 {
+    f(a, b)
+}
+
+fn main() {
+    let result = apply(|x, y| x + y, 10, 32);
+    assert_eq!(result, 42);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected
deleted file mode 100644
index a6b62b249..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected
+++ /dev/null
@@ -1,15 +0,0 @@
-
-┌─ 1 (root, init)
-│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│   span: 0
-│
-│  (142 steps)
-└─ 3 (stuck, leaf)
-    #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
-    span: 157
-
-
-┌─ 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 0de9ce097..5f36b155d 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -62,7 +62,6 @@
     'test_offset_from-fail',
     'ref-ptr-cast-elem-fail',
     'ref-ptr-cast-elem-offset-fail',
-    'and_then_closure-fail',
 ]