Theorem: AIG.relabel_size_eq_size (LeanSAT/AIG/Relabel.lean)

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