[isabelle] Prove by instantiation



Hello

For the following:

axiomatization
c :: real
where
ax1 : "c > 0"

lemma "EX z. c = z"
sorry

Can the quantifier be proved by instantiation only? Perhaps, this
question logically follows: is there an expression y such that apply
(rule exI [where x=y])?

Thank you for the help.

John





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