[Logiweb] Re: Quantifier elimination leads to variable clash

[Ole Hyldahl Hansen]

On Mon, 20 Jun 2005, Anders B0ggild-Povlsen wrote:

> If I remenber correctly, Klaus suggested that you prove the lemma with any 
> free meta variables and use that lemma to prove the same thing using the meta 
> variables you wanted to use in the first place.
>
> In your case you could begin by proving (D=>E) => (D=>F=>E) and use that 
> lemma to prove (A => B) => (A => C => B). That should avoid variable clash.

You're right. That was indeed the suggestion. At least it should work for 
now. Thanks for reminding me.

Ole