let A := {x : N0 | motive x}
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
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}
⊢ motive x