have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  specialize hs n
  exact hs hel
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
⊢ 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
⊢ motive x