rw [relabel_unsat_iff]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ (relabel
          (fun x =>
            match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0)
          aig).unsatAt
      idx hidx1 ↔
    aig.unsatAt idx hidx2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ ∀ (x y : α),
    x ∈ aig →
      y ∈ aig →
        ((match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0) =
            match (RelabelNat.State.ofAIG aig).find? y with
            | some var => var
            | none => 0) →
          x = y