∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {start : ℕ} {assign : α → Bool} {invert : Bool} {a : α}
  {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size},
  aig.decls[start] = Std.Sat.AIG.Decl.atom a →
    ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = (assign a ^^ invert)