rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]
no goals