Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 28 May 1993 11:07:50 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02621;
          Fri, 28 May 93 02:43:29 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA02616;
          Fri, 28 May 93 02:43:18 -0700
Message-Id: <9305280943.AA02616@ted.cs.uidaho.edu>
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <24766-0@iraun1.ira.uka.de>; Fri, 28 May 1993 09:41:32 +0200
Date: Fri, 28 May 93 9:42:55 MET DST
From: reetz <reetz@ira.uka.de>
To: info-hol@ted.cs.uidaho.edu
Subject: Elemination of @-terms

Dear all!
I would like to proof the following goal:

([],--`(@m. ?vn. (m = F) /\ (vn = vn1)) = F`--);

I was already able to proof the following three
goals:

TAC_PROOF (([],--`?m.?vn.(m=F) /\ (vn=vn1)`--),
  EVERY [ 
    EXISTS_TAC (--`F`--),
    EXISTS_TAC (--`vn1`--),
    EQ_finite_type_TAC (theorem "demo_fgm" "VN")
  ]);
SELECT_RULE it;
SELECT_CONV (concl it);

But how can I use them to proof my goal? (Don't worry
about vn=vn1, this is just an example...)

Thanks in advance! :)

Ralf

(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                 SFB 358 of the german research society (DFG)  *)
(*  reetz@ira.uka.de           University of Karlsruhe, Germany              *)
(*                                                                           *)
(*****************************************************************************)