Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <16105-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 16:39:55 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11757;
          Fri, 24 Jul 92 08:29:43 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA11752;
          Fri, 24 Jul 92 08:29:37 -0700
Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA08874;
          Fri, 24 Jul 92 11:32:03 -0400
Message-Id: <9207241532.AA08874@air52.larc.nasa.gov>
Date: Fri, 24 Jul 92 11:32:03 -0400
From: Victor "A." Carreno <vac@gov.nasa.larc.air16>
To: info-hol@edu.uidaho.cs.ted

Hi,

I don't know if this is more clever:

g  "!P:*->bool. !Q R (St:(*->bool)->(*->bool)).
  (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)";;

e (REPEAT STRIP_TAC);;
e (RES_TAC);;
e (RES_TAC);;

proves the goal.

Victor.