. next hcase1 =>
  split at heq
  . next hcase2 =>
    apply RelabelNat.State.ofAIG_find_unique
    . assumption
    . rw [heq]
      assumption
  . next hcase2 =>
    exfalso
    rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
    simp[hcase2] at hn
case h_1
α : 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
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

case h_2
α : 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
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
case h_2
α : 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
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y