# Re: [isabelle] A simple lemma

On Fri, Sep 7, 2012 at 9:25 AM, John Munroe <munddr at gmail.com> wrote:
> Hi,
>
> Does anyone know why the following lemma is provable?
>
> lemma "F = G --> (EX a b. a ~= b --> F a = G a & F b ~= G b)"
> by auto
>
> If F and G are equal, then F x = G x for all x. So how come the above
> is provable?
Your lemma is provable even without the "F = G":
lemma "EX a b. a ~= b --> F a = G a & F b ~= G b"
by auto
The proof is by instantiating "a" and "b" with the same value. Then
you get "False --> something", which simplifies to True.
I think you may have meant to say this instead:
lemma "F = G --> (EX a b. a ~= b & F a = G a & F b ~= G b)"
which is indeed unprovable.
- Brian

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