simp [heq, h]
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : f x = a
⊢ decls[idx] = atom x ∧ a = f x
no goals