Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <15062-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 15:51:00 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11710; Fri, 24 Jul 92 07:42:19 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA11705; Fri, 24 Jul 92 07:42:13 -0700 Received: by infix.cs.ruu.nl id AA21267 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Fri, 24 Jul 1992 16:43:19 +0200 From: Wishnu Prasetya Message-Id: <199207241443.AA21267@infix.cs.ruu.nl> Subject: How to prove this shortly? To: info-hol@edu.uidaho.cs.ted (hol mailing list) Date: Fri, 24 Jul 92 16:43:18 METDST X-Mailer: ELM [version 2.3 PL11] Hi there! 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? Thank you kindly. -Wishnu Prasetya-