# [isabelle] obtain command failure

```Hi
```
I have a small problem with obtain - it fails with predicate " x : Set" and some values of Set.
```
definition inx :: "('a  * nat ) set"
where " inx  = {z. EX  s n.((s:: 'a) ,n)= z }"
lemma  "~ (EX  e. e :  inx)"
proof
assume as:  "EX x. x : inx" show False
proof -
from as  obtain x where "x : inx" ..  --"NOT OK"

But the expanded existential elimination works

lemma  "~ (EX  e. e :  inx)"
proof
assume as:  "EX x. x : inx" show False
proof -
from as  show ?thesis
proof
fix x   assume "x : inx" show ?thesis    --"OK"
oops

```
And wit a small change to the definition of the set the obtain command works.
```
definition inw :: "(nat * nat) set"
where " inw  = {z. EX n . (1,n) = z }"

lemma  "~ (EX  e. e :  inw)"
proof
assume as:  "EX x. x : inw" show False
proof -
from as  obtain x where "x : inw" ..  --"OK"
oops

```
Hope this is helpful and I have not slipped up some where. Example is in attached file.
```
kind regards

```
```theory ex
imports Main
begin

definition inw :: "(nat * nat) set"
where " inw  = {z. EX n . (1,n) = z }"

definition inx :: "('a  * nat ) set"
where " inx  = {z. EX  s n.((s:: 'a) ,n)= z }"

lemma  "~ (EX  e. e :  inw)"
proof
assume as:  "EX x. x : inw" show False
proof -
from as  obtain x where "x : inw" ..  --"OK"
oops

lemma  "~ (EX  e. e :  inx)"
proof
assume as:  "EX x. x : inx" show False
proof -
from as  show ?thesis
proof
fix x   assume "x : inx" show ?thesis --"OK"
oops

lemma  "~ (EX  e. e :  inx)"
proof
assume as:  "EX x. x : inx" show False
proof -
from as  obtain x where "x : inx" ..  --"NOT OK"
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.