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; Tue, 10 May 1994 23:55:42 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA11451;
          Tue, 10 May 1994 16:42:40 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA11437;
          Tue, 10 May 1994 16:42:35 -0600
Received: from ice.cs.ucdavis.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA10420;
          Tue, 10 May 1994 15:43:32 -0700
Received: by ice.cs.ucdavis.edu (5.65/UCD.CS.2.5) id AA11792;
          Tue, 10 May 1994 15:43:32 -0700
Date: Tue, 10 May 1994 15:43:32 -0700
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9405102243.AA11792@ice.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: Lists in HOL


Howdy.

Within HOL, is the following term provably false?

? (i:num) . 17 = EL i []

My understanding is that, with the given axiomatization of lists, you
can't say anything about, say, element twelve of the empty list (other
than it is the same as element 13 of [1]). 

Email, please. Thanx.

Rob