Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <20364-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 13:44:25 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14602; Mon, 27 Jul 92 05:32:37 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA14597; Mon, 27 Jul 92 05:32:28 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <20009-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 13:24:17 +0100 To: Victor "A." Carreno Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl In-Reply-To: Your message of Fri, 24 Jul 92 11:32:03 -0400. <9207241532.AA08874@air52.larc.nasa.gov> Date: Mon, 27 Jul 92 13:24:08 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.014:27.06.92.12.24.30"@cl.cam.ac.uk> Another proof, not necessarily better than using RES_TAC but also of interest, of the goal "!P:*->bool. !Q R (St:(*->bool)->(*->bool)). (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)" is REPEAT STRIP_TAC THEN REPEAT (FIRST_ASSUM MATCH_MP_TAC) THEN FIRST_ASSUM ACCEPT_TAC Tom