diff --git a/proof/refine/Invariants_H.thy b/proof/refine/Invariants_H.thy
index a604745dd2..2b65be43b4 100644
--- a/proof/refine/Invariants_H.thy
+++ b/proof/refine/Invariants_H.thy
@@ -1507,8 +1507,10 @@ lemma (in Arch) tcb_cte_cases_distinct_n:
 requalify_facts Arch.tcb_cte_cases_distinct_n
 
 lemmas tcb_cte_cases_neqs_n =
-  tcb_cte_cases_distinct_n[simplified]
-  distinct_rev[THEN iffD2, OF tcb_cte_cases_distinct_n, simplified]
+  conjI[OF
+    tcb_cte_cases_distinct_n[simplified]
+    distinct_rev[THEN iffD2, OF tcb_cte_cases_distinct_n, simplified],
+    simplified conj_ac, simplified] (* remove duplicates from 0/1 simplification *)
 
 lemma tcb_cte_cases_simps[simp]:
   "tcb_cte_cases 0  = Some (tcbCTable, tcbCTable_update)"
@@ -1516,7 +1518,6 @@ lemma tcb_cte_cases_simps[simp]:
   "tcb_cte_cases (2 << cteSizeBits) = Some (tcbReply, tcbReply_update)"
   "tcb_cte_cases (3 << cteSizeBits) = Some (tcbCaller, tcbCaller_update)"
   "tcb_cte_cases (4 << cteSizeBits) = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)"
-  (* FIXME arch-split: warning due to tcb_cte_cases_neqs overlapping *)
   by (simp add: tcb_cte_cases_neqs_n tcb_cte_cases_def)+
 
 lemmas tcbSlot_defs = tcbCTableSlot_def tcbVTableSlot_def tcbReplySlot_def tcbCallerSlot_def
@@ -1529,7 +1530,6 @@ lemma tcb_cte_cases_distinct:
      tcbReplySlot << cteSizeBits,
      tcbCallerSlot << cteSizeBits,
      tcbIPCBufferSlot << cteSizeBits]"
-  (* FIXME arch-split: warning due to tcb_cte_cases_neqs overlapping *)
   by (simp add: tcbSlot_defs tcb_cte_cases_neqs_n)
 
 lemmas tcb_cte_cases_neqs =