diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 5839521b4..4d10f37ca 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1838,24 +1838,15 @@ the safety of this cast. The logic of the semantics and saftey of this cast for
 ```k
   syntax MIRError ::= "#UBInvalidTransmuteMaybeUninit"
   rule <k>
-           #cast( _VAL:Value , castKindTransmute , TY_FROM , TY_TO )
+           #cast( VAL:Value , castKindTransmute , _TY_FROM , TY_TO )
         =>
-           #UBInvalidTransmuteMaybeUninit
+           Union(fieldIdx(1), Aggregate(variantIdx(0), ListItem(VAL) .List))
        ...
       </k>
       requires #isUnionType(lookupTy(TY_TO))
         andBool #typeNameIs(lookupTy(TY_TO), "std::mem::MaybeUninit<")
-        andBool TY_FROM =/=K getFieldTy(#lookupMaybeTy(getFieldTy(lookupTy(TY_TO), 1)), 0)
-
-  rule <k>
-           #cast( VAL:Value , castKindTransmute , TY_FROM , TY_TO )
-        =>
-           Union( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem(VAL) .List ))
-       ...
-      </k>
-      requires #isUnionType(lookupTy(TY_TO))
-        andBool #typeNameIs(lookupTy(TY_TO), "std::mem::MaybeUninit<")
-        andBool TY_FROM ==K getFieldTy(#lookupMaybeTy(getFieldTy(lookupTy(TY_TO), 1)), 0)
+  // `MaybeUninit<T>` accepts arbitrary bit patterns, so any value can be
+  // reinterpreted into the union's initialized field.
 
   // Converting static or dynamic sized array of `T` to array of `std::mem::MaybeUninit<T>`.
   // FIXME: Might need to check sizes as this cast could come from transmute_unchecked
diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected
deleted file mode 100644
index 12948003f..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected
+++ /dev/null
@@ -1,17 +0,0 @@
-
-┌─ 1 (root, init)
-│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│   span: 0
-│
-│  (16 steps)
-└─ 3 (stuck, leaf)
-    #ProgramError ( #UBInvalidTransmuteMaybeUninit )
-~> #freezer#setLocalValue(_,_)_
-    function: main
-    span: 60
-
-
-┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-i128.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-i128.main.expected
new file mode 100644
index 000000000..20e9eaff3
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-i128.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (77 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-i128.rs
similarity index 74%
rename from kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-i128.rs
index 6207a3a7b..57d853530 100644
--- a/kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-fail.rs
+++ b/kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-i128.rs
@@ -4,7 +4,6 @@ use std::mem::MaybeUninit;
 fn main() {
     unsafe {
         let maybe_unsigned = std::intrinsics::transmute::<i128, MaybeUninit::<u128>>(9999);
-                                  // Note different types ^^^^                ^^^^
         assert!(maybe_unsigned.assume_init() == 9999);
     }
 }
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 14b5221c3..c622cb4fd 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -60,7 +60,7 @@
     'assert-inhabited-fail',
     'iterator-simple',
     'unions-fail',
-    'transmute-maybe-uninit-fail',
+    'transmute-maybe-uninit-i128',
     'ptr-through-wrapper-fail',
     'test_offset_from-fail',
     'ref-ptr-cast-elem-fail',