[isabelle] introduction rule for order bounded quantifiers.


I have a question about order bounded quantifiers.

I have a goal like "i <= n ==> \<exists> j <= Suc n. x ^ j = x ^ i"
which should be trivial by instantiating j with i, however using
(rule_tac x = i in exI) does not work. What is the introduction
theorem for this kind of quantifiers? Where is this theorem

Best regards,

Viorel Preoteasa

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