Re: [isabelle] A simple lemma


If you rewrite it like:

lemma "F = G --> (EX a b. a = b  or (F a = G a & F b ~= G b))"

you would see why it is true.


On 9/7/12 7:25 PM, John Munroe wrote:

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?

Thanks a lot for your time.


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