exists (ofAIGAux aig).max
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∃ n, State.Inv1 n (ofAIG aig)
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)