simp only [mem_def] at ha
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig).find? a = some n
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig).find? a = some n