next heq1 =>
rw [denote_mkConst_cached heq1]
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧
no goals