rcases Array.get_of_mem ha with ⟨⟨i, isLt⟩, hi⟩
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig).find? a = some n
case intro.mk
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ∃ n, (ofAIG aig).find? a = some n