Theorem: AIG.RelabelNat.State.Inv2.upper_lt_size (LeanSAT/AIG/RelabelNat.lean)

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
upper : Nat
map : HashMap α Nat
decls : Array (Decl α)
hinv : Inv2 decls upper map
⊢ upper ≤ decls.size
Tactic:
cases hinv <;> omega
State after:
no goals