From dc8d0fc140ba531d2f0bad60b9be2991f7a6475b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 08:24:57 +0000 Subject: [PATCH] t renamed to t' since t was already defined in the same file --- helm/matita/tests/elim.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma index 1d874def3..9d48bc970 100644 --- a/helm/matita/tests/elim.ma +++ b/helm/matita/tests/elim.ma @@ -62,7 +62,7 @@ alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". inductive sum (n:nat) : nat \to nat \to Set \def k: \forall x,y. n = x + y \to sum n x y. -theorem t: \forall x,y. \forall H: sum x y O. +theorem t': \forall x,y. \forall H: sum x y O. match H with [ (k a b p) \Rightarrow a ] = x. intros. cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x). -- 2.39.2