simp
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size
no goals