∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {aig : Std.Sat.AIG α} {r : α → β}, (Std.Sat.AIG.relabel r aig).decls.size = aig.decls.size