Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Mon, 8 Mar 1993 22:35:16 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16433; Mon, 8 Mar 93 14:16:22 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from scylla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA16428; Mon, 8 Mar 93 14:15:45 -0800 Received: from sparta.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) id AA28717; Mon, 8 Mar 93 17:14:48 EST Date: Mon, 8 Mar 93 17:14:41 EST From: shb@com.oracorp Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA05144; Mon, 8 Mar 93 17:14:41 EST Message-Id: <9303082214.AA05144@sparta.oracorp.com> To: info-hol@edu.uidaho.cs.ted Subject: Way around X_FUN_EQ_CONV restriction? Is there any reasonably convenient way around the restriction in X_FUN_EQ_CONV to using a single variable in replacing function equality with an extensionally equivalent universal equality of terms? I'm trying to show equality of complicated functions given by lambda expressions, functions whose arguments are pairs, and for clarity I'd like to give meaningful names to the components of arbitrary arguments to these functions, not simply have them as FST p and SND p for an arbitrary pair named p; I'd then prove equality for all possible values of all the components. There ought to be an easy way to do this, but I haven't been able to find it. Steve Brackin ORA