diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 833f2d65733983324ed383430538b92620b953a9..1a4a23362360caa54ad1be6ae0a96ba3543fb039 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -1679,7 +1679,7 @@ app_ok fun_ok primop_ok fun args
                   -- and we'd need to actually test n_val_args == 0.)
 
          -- Functions that terminate fast without raising exceptions etc
-         -- See Note [Discarding unnecessary unsafeEqualityProofs]
+         -- See (U12) of Note [Implementing unsafeCoerce]
          | fun `hasKey` unsafeEqualityProofIdKey -> True
 
          | otherwise -> False
@@ -1876,20 +1876,6 @@ GHC.Builtin.PrimOps.
 Note that exprIsHNF /can/ and does take advantage of evaluated-ness;
 it doesn't have the trickiness of the let-can-float invariant to worry about.
 
-Note [Discarding unnecessary unsafeEqualityProofs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In #20143 we found
-   case unsafeEqualityProof @t1 @t2 of UnsafeRefl cv[dead] -> blah
-where 'blah' didn't mention 'cv'.  We'd like to discard this
-redundant use of unsafeEqualityProof, via GHC.Core.Opt.Simplify.rebuildCase.
-To do this we need to know
-  (a) that cv is unused (done by OccAnal), and
-  (b) that unsafeEqualityProof terminates rapidly without side effects.
-
-At the moment we check that explicitly here in exprOkToDiscard,
-but one might imagine a more systematic check in future.
-
-
 ************************************************************************
 *                                                                      *
              exprIsHNF, exprIsConLike
@@ -1973,6 +1959,9 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like
       | isValArg a               = app_is_value e 1
       | otherwise                = is_hnf_like e
     is_hnf_like (Let _ e)        = is_hnf_like e  -- Lazy let(rec)s don't affect us
+    is_hnf_like (Case e b _ as)
+      | Just rhs <- isUnsafeEqualityCase e b as
+      = is_hnf_like rhs
     is_hnf_like _                = False
 
     -- 'n' is the number of value args to which the expression is applied
diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index 368c204f471b56eeb0e3d2bb8a93c3e46a4c6918..e1b00ce10d7175630356d565f7278d3a438d1fa5 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -73,16 +73,7 @@ Now our bad case can't happen.  We'll have
         UnsafeRefl (co :: t1 ~ t2) -> ....(x |> co)....
 
 and the (x |> co) mentions the evidence 'co', which prevents it
-floating.
-
-But what stops the whole (case unsafeEqualityProof of ...) from
-floating?  Answer: we never float a case on a redex that can fail
-outside a conditional.  See Primop.hs,
-Note [Transformations affected by primop effects].
-And unsafeEqualityProof (being opaque) is definitely treated as
-can-fail.
-  (Huh? It seems we have a special-case in exprOkForSpeculation (app_ok)
-   /specifically/ allowing unsafeEqualityProof.  Something smells wrong. #23754)
+floating. See also wrinkle (U11) below.
 
 While unsafeCoerce is a perfectly ordinary function that needs no
 special treatment, Unsafe.Coerce.unsafeEqualityProof is magical, in
@@ -215,6 +206,22 @@ There are yet more wrinkles
       the kind-/homogeneous/ unsafeEqualityProof twice.
 
       See Note [Wiring in unsafeCoerce#] in Desugar.
+
+(U11) But what stops the whole (case unsafeEqualityProof of ...) from
+      being speculated out of a conditional? (E.g., strict float out.)
+      Answer: we never float a case on something that is not an HNF
+      ('exprIsHNF') outside a conditional.
+      See Note [Floating single-alternative cases].
+
+(U12) In #20143 we found
+         case unsafeEqualityProof @t1 @t2 of UnsafeRefl cv[dead] -> blah
+      where 'blah' didn't mention 'cv'.  We'd like to discard this
+      redundant use of unsafeEqualityProof, via GHC.Core.Opt.Simplify.rebuildCase.
+      To do this we need to know
+        (a) that cv is unused (done by OccAnal), and
+        (b) that unsafeEqualityProof terminates rapidly without side effects.
+      At the moment we check that explicitly in GHC.Core.Utils.exprOkToDiscard,
+      but one might imagine a more systematic check in future.
 -}
 
 -- | This type is treated magically within GHC. Any pattern match of the