diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean
index f6b2665d6d..12abc2d657 100644
--- a/src/Std/Sat/AIG/Relabel.lean
+++ b/src/Std/Sat/AIG/Relabel.lean
@@ -128,7 +128,21 @@ theorem unsat_relabel {aig : AIG α} (r : α → β) {hidx} :
   specialize h (assign ∘ r)
   simp [h]
 
-theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
+theorem relabel_unsat_iff_of_not_Nonempty {aig : AIG α}
+    {r : α → β} {hidx1} {hidx2}
+    (hNonempty : ¬ Nonempty α) :
+    (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
+  constructor
+  · intro hα assignα
+    let assignβ : β → Bool := fun b => false
+    specialize hα assignβ
+    have hAssignα : assignα  = assignβ ∘ r := by
+      ext a
+      apply hNonempty (Nonempty.intro a) |>.elim
+    rw [hAssignα, ← denote_relabel, ← hα]
+  · apply unsat_relabel
+
+theorem relabel_unsat_iff_of_Nonempty [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
     (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
     (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
   constructor
@@ -154,6 +168,16 @@ theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {
         contradiction
   · apply unsat_relabel
 
+/--
+`relabel` preserves unsatisfiablility.
+-/
+theorem relabel_unsat_iff {aig : AIG α} {r : α → β} {hidx1} {hidx2}
+    (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
+    (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
+  by_cases hαNonempty : Nonempty α
+  · apply relabel_unsat_iff_of_Nonempty hinj
+  · apply relabel_unsat_iff_of_not_Nonempty hαNonempty
+
 namespace Entrypoint
 
 def relabel (r : α → β) (entry : Entrypoint α) : Entrypoint β :=
diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean
index 1490b9506b..5508ae9097 100644
--- a/src/Std/Sat/AIG/RelabelNat.lean
+++ b/src/Std/Sat/AIG/RelabelNat.lean
@@ -325,10 +325,7 @@ theorem relabelNat'_fst_eq_relabelNat {aig : AIG α} : aig.relabelNat'.fst = aig
 theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig.decls.size := by
   simp [relabelNat, relabelNat']
 
-/--
-`relabelNat` preserves unsatisfiablility.
--/
-theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
+theorem relabelNat_unsat_iff_of_NonEmpty [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
     (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
   dsimp only [relabelNat, relabelNat']
   rw [relabel_unsat_iff]
@@ -350,6 +347,15 @@ theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
     rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
     simp [hcase] at hn
 
+/--
+`relabelNat` preserves unsatisfiablility.
+-/
+theorem relabelNat_unsat_iff {aig : AIG α} {hidx1} {hidx2} :
+    (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
+  by_cases hNonempty : Nonempty α
+  · apply relabelNat_unsat_iff_of_NonEmpty
+  · apply relabel_unsat_iff_of_not_Nonempty hNonempty
+
 namespace Entrypoint
 
 def relabelNat' (entry : Entrypoint α) : (Entrypoint Nat × HashMap α Nat) :=
@@ -375,7 +381,7 @@ def relabelNat (entry : Entrypoint α) : Entrypoint Nat :=
 /--
 `relabelNat` preserves unsatisfiablility.
 -/
-theorem relabelNat_unsat_iff {entry : Entrypoint α} [Nonempty α] :
+theorem relabelNat_unsat_iff {entry : Entrypoint α} :
     (entry.relabelNat).Unsat ↔ entry.Unsat:= by
   simp only [Unsat, relabelNat]
   rw [AIG.relabelNat_unsat_iff]