From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 16 Nov 2011 15:15:13 +0000 (+0000)
Subject: inversion replaced by elim (???)
X-Git-Tag: make_still_working~2103
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f110058b4445285a17447ca46211259349764c84;p=helm.git

inversion replaced by elim (???)
---

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)).