rw [← relabel_size_eq_size (f := f)]
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < aig.decls.size
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel f aig).decls.size