# Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails

Just for fun some further vacuous 'obtain' proofs:
notepad
begin
obtain x where "x = (0 :: nat)" by (rule that) (rule refl)
next
obtain x where "x == (0 :: nat)" by (rule that) (rule reflexive)
next
obtain x where "x == (0 :: nat)" ..
end

`The last form works, because "that" is declared as Pure.intro, and Pure
``"reflexive" implicit (like assumption).
`
The better form is this:
def x == "0 :: nat"

`Here the system does the reflexicity step for you, and it bypasses the
``full "may-assume-that-holds" mechanism of 'obtain', that involves the
``restriction on variable occurrences (as seen in the exE rule).
`
Makarius

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