simp [relabel]
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
entry : Entrypoint α
f : α → β
⊢ (relabel f entry).aig.decls.size = entry.aig.decls.size
no goals