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)"
If F and G are equal, then F x = G x for all x. So how come the above
Thanks a lot for your time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and