intro x y hx hy heq
α : 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
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
heq :
  (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