Simple Subtype

Stream: Is there code for X?

[Marcus Rossel]

Let i : { x : ℕ // ∃ (h : p x), q x } for some propositions p and q over ℕ.
Is there a way to extract an instance i' : { x : ℕ // p x } from this (allowing classical)?
Or else, is there a nice way of getting to i' starting with just ∃ (h : p x), q x?

[Eric Wieser]

Your second question is missing the binder that introduces x

[Eric Wieser]

But I think the answer to the first is simply let \<i', hi'\> := i in \<i', let \<hp, hq\> := hi' in hp\>

[Eric Wieser]

You have to destructure the two parts separately, rather than using let \<i', hp, hq\> := i which will give an error about elimination not being into prop

[Eric Wieser]

(\< is the vs-code input shortcut)

[Yury G. Kudryashov]

I think, ⟨i, i.2.snd⟩ should work.