Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 21 Sep 1993 10:33:36 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA17736;
          Tue, 21 Sep 93 02:23:03 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA17732; Tue, 21 Sep 93 02:22:59 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA13389;
          Tue, 21 Sep 93 02:23:04 -0700
Message-Id: <9309210923.AA13389@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: A simple question
Date: Tue, 21 Sep 93 02:23:02 PDT
From: chou@cs.ucla.edu

Suppose that

    ~(NULL x)

is among the assumptions of my goal, where x may be a complex term.
I wish to add the following conclusion to the assumption list:

    x = CONS h t

where h and t are two fresh variables, using the following theorem:

    |- !l. NULL l \/ (?h t. l = CONS h t)

What is the simplest way to do this?

The simplest way I can think of is to first rewrite the theorem above
into the following form:

    |- !l. ~(NULL l) ==> (?t h. l = CONS h t)

and then use IMP_RES_TAC.

- Ching Tsun