inversion replaced by elim (???)

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index c1b9c77c03c85a8cc739b6542b81563eebc37b22..d17dcca7ec4fc727e5503e75f21cc0be8d3e0ca8 100644 (file)
--- 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)).