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