simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : (∃ (x_1 : ↑x ∈ N0), motive { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔ ↑x ∈ N0
⊢ motive x
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : motive x
⊢ motive x