[isabelle] A simple lemma


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.