. intro h assign
  have em := Classical.propDecidable
  let g : β → α := fun b =>
    if h:∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice inferInstance
  have h' := unsat_relabel g h
  specialize h' assign
  simp only [denote_relabel] at h'
  rw [← h']
  apply denote_congr
  . intro a hmem
    simp [g]
    split
    . next h =>
      rcases Exists.choose_spec h with ⟨_, heq⟩
      specialize hinj _ _ (by assumption) (by assumption) heq
      simp [hinj]
    . next h =>
      simp only [not_exists, not_and] at h
      specialize h a hmem
      contradiction
case mp
α : 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
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2

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
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