intros
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
⊢ aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧