rw [AIG.relabelNat_unsat_iff]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.aig.relabelNat.unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯
no goals