rw [denote_idx_const heq2]
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
heq2 : aig.decls[start] = Decl.const b
⊢ b = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
no goals