using exists

Stream: new members

[bulut]

say i have a prop of the form \exists k, 2*k = x, and I want to "bind" k to use it - how to do this?

[Patrick Massot]

We need more context. Are you using term mode or tactic mode? What do you mean by "I have a prop"?

[Chris Hughes]

does cases h where h : Exists k, 2 * k = x do what you want? In term mode you can do let \<k, hk\> := h in

[bulut]

I'm sorry- I should have been more clear. I'm using tactic mode, and have a proposition of type ∃ (k : ℕ), 2 * k = x, and I want to bind k to a variable.

[bulut]

I will try cases now

[Patrick Massot]

Then the first part of Chris' answer is what you want

[Patrick Massot]

Assuming your assumption is called h (since you didn't want to disclose this information) then you can write cases h with k hk,