∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {v : α} {assign : α → Bool} {aig : Std.Sat.AIG α}
  {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom v)},
  aig.cache.get? (Std.Sat.AIG.Decl.atom v) = some hit →
    ⟦assign, { aig := aig, ref := { gate := hit.idx, invert := false, hgate := ⋯ } }⟧ = ⟦assign, aig.mkAtom v⟧