From f110058b4445285a17447ca46211259349764c84 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 16 Nov 2011 15:15:13 +0000
Subject: [PATCH] inversion replaced by elim (???)

---
 matita/matita/lib/basics/star.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index c1b9c77c0..d17dcca7e 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -107,7 +107,7 @@ inductive equiv (A:Type[0]) (R:relation A) : A → A → Prop ≝
   
 theorem trans_equiv: ∀A,R,a,b,c. 
   equiv A R a b → equiv A R b c → equiv A R a c.
-#A #R #a #b #c #Hab #Hbc (inversion Hbc) /2/
+#A #R #a #b #c #Hab #Hbc (elim Hbc) /2/
 qed.
  
 theorem equiv_equiv: ∀A,R. exteqR … (equiv A R) (equiv A (equiv A R)).
-- 
2.39.2