apply Inv1.property <;> assumption
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n✝
a' : α
ha' : (ofAIG aig).find? a' = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'
no goals