Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <15671-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 16:23:50 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11718; Fri, 24 Jul 92 08:10:35 -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 AA11713; Fri, 24 Jul 92 08:10:28 -0700 Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <15464-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 16:11:03 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Wai.Wong@uk.ac.cam.cl Subject: Re: How to prove this shortly? In-Reply-To: Your message of Fri, 24 Jul 92 16:43:18 +0700. <199207241443.AA21267@infix.cs.ruu.nl> Date: Fri, 24 Jul 92 16:10:53 +0100 From: Wai Wong Message-Id: <"swan.cl.ca.485:24.06.92.15.11.26"@cl.cam.ac.uk> Wishnu writes: > I'm trying to prove the following 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)" > I'm not satisfied with the proof I made since it is somewhat lengthy. > The goal seems simple, there must be a cleverer way to prove it, so I > thought. Perhaps anyone can suggest me a good one? The following tactic should solve the goal: REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC Wai