apply unsat_relabel
case mpr
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ aig.unsatAt idx hidx2 → (relabel f aig).unsatAt idx hidx1
no goals