∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f] {assign : α → Bool}
  (entry : Std.Sat.AIG.Entrypoint α) {input : β entry.aig} {h : entry.ref.gate < (f entry.aig input).aig.decls.size},
  ⟦assign,
      { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, invert := entry.ref.invert, hgate := h } }⟧ =
    ⟦assign, entry⟧