Re: [isabelle] Weird nesting of Quantifiers



Try this:

	apply (simp flip: ex_simps all_simps)

Your example is a rare case in which prenexing is actually a good idea.

Larry

> On 14 Feb 2021, at 15:44, Peter Lammich <lammich at in.tum.de> wrote:
> 
> Is there any way, e.g. a simproc or so, to automate this process, or is
> my only solution to bloat up the otherwise fully automatic proofs by
> those weird auxiliary lemmas (of which I could, of course, prove
> instances for the most common cases globally and add them to the
> simpset) 





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