∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (gate : aig.Ref)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkNotCached gate).aig.decls.size},
  (aig.mkNotCached gate).aig.decls[idx] = aig.decls[idx]