*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] A simple lemma*From*: John Munroe <munddr at gmail.com>*Date*: Fri, 7 Sep 2012 17:25:52 +0100

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? Thanks a lot for your time. John

**Follow-Ups**:**Re: [isabelle] A simple lemma***From:*Brian Huffman

**Re: [isabelle] A simple lemma***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Defining equality for a new type
- Next by Date: Re: [isabelle] A simple lemma
- Previous by Thread: Re: [isabelle] Defining equality for a new type
- Next by Thread: Re: [isabelle] A simple lemma
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list