From a840c90571f0d819593405c389728c2c65e24e61 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Mar 2008 13:02:05 +0000 Subject: [PATCH] removed pointless test --- .../matita/tests/coercions_dupelim.ma | 31 ------------------- 1 file changed, 31 deletions(-) delete mode 100644 helm/software/matita/tests/coercions_dupelim.ma diff --git a/helm/software/matita/tests/coercions_dupelim.ma b/helm/software/matita/tests/coercions_dupelim.ma deleted file mode 100644 index 5c1c0c9f8..000000000 --- a/helm/software/matita/tests/coercions_dupelim.ma +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - - - -include "nat/nat.ma". - -axiom A : Type. - -inductive vec : nat -> Type := - | vnil : vec O - | vcons : ∀x:A.∀n:nat. vec n -> vec (S n). - -definition f := λx,n.λv:vec n.vcons x n v. -definition g := λn,x.λv:vec n.vcons x n v. - -include "logic/equality.ma". - -(* definition xx := f = g. *) -theorem xx1 : ∀n.∀x1:vec n.f ? ? x1 = g ? ? x1. -- 2.39.2