simp[hcase] at hn
case intro
α : 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
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? x = some n
⊢ False
no goals