From a1675f3cb3c4df7d334dffda1d33aaa973899814 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Jul 2006 11:52:51 +0000 Subject: [PATCH 1/1] le_inv renamed to avoid conflicts with the automatically generated one. --- helm/software/matita/tests/inversion2.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/tests/inversion2.ma b/helm/software/matita/tests/inversion2.ma index 65dc75d40..f3bc943aa 100644 --- a/helm/software/matita/tests/inversion2.ma +++ b/helm/software/matita/tests/inversion2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/inversion/". +set "baseuri" "cic:/matita/tests/inversion2/". include "legacy/coq.ma". inductive nat : Set \def @@ -24,7 +24,7 @@ inductive le (n:nat) : nat \to Prop \def leO : le n n | leS : \forall m. le n m \to le n (S m). -theorem le_inv: +theorem le_inv2: \forall n,m. \forall P: nat -> nat -> Prop. ? -> ? -> le n m -> P n m. -- 2.39.2