Theorem: AIG.Entrypoint.relabelNat_unsat_iff (LeanSAT/AIG/RelabelNat.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.relabelNat.unsat ↔ entry.unsat
Tactic:
simp [relabelNat, unsat]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.aig.relabelNat.unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯

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