Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 8 Oct 1994 16:54:48 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA22624;
          Sat, 8 Oct 1994 09:50:52 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from emu.pmms.cam.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA22620;
          Sat, 8 Oct 1994 09:50:50 -0600
Received: by emu.pmms.cam.ac.uk (UK-Smail 3.1.25.1/1); Sat, 8 Oct 94 16:43 BST
Message-Id: <m0qtdvQ-0003UaC@emu.pmms.cam.ac.uk>
Date: Sat, 8 Oct 94 16:43 BST
From: Thomas Forster <T.Forster@pmms.cam.ac.uk>
To: chou@cs.ucla.edu, tfm@dcs.gla.ac.uk
Subject: Re: A Little Puzzle.
Cc: info-hol@leopard.cs.byu.edu

Certainly the easy thing is to Skolemise.   From a logical point
of view this is extravagant.  The correct way to prove this is
to use a $\exists$-elimination rule like
                         F(x)
                          .
                          .
         (\exists y)(Fy)  p
         ------------------
                  p

and then you don't have to skolemise.  This illustrates the way in
which HOL uses AC all the time.  Not very nice.....
             
            Thomas